🚀 go-pugleaf

In article <ALTI.92Nov16194749@tanera.dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:

   Certainly, but this just means that you have to give up something to
   get classical reasoning AND propositions as types. I am not an expert
   in this area but as I understand it: You may have a computational
   interpretation of type theory if you 'fix' your evaluation strategy
		     ^^^^^^^^^^^
Should read: classical logic

   (i.e. you decide to use only the equations of the call-by-value
   \lambda calculus). 

Sorry.
--

 Thorsten Altenkirch         	And there's a hand, my trusty fiere,
 Laboratory for Foundations  	   And gie's a hand o' thine,
 of Computer Science 	      	And we'll tak a right guid-willie waught
 University of Edinburgh     	   For auld lang syne!