home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2068 < prev    next >
Encoding:
Internet Message Format  |  1992-11-17  |  1.5 KB
  1. Path: sparky!uunet!charon.amdahl.com!pacbell.com!sgiblab!zaphod.mps.ohio-state.edu!uwm.edu!biosci!agate!doc.ic.ac.uk!uknet!edcastle!dcs.ed.ac.uk!alti
  2. From: alti@dcs.ed.ac.uk (Thorsten Altenkirch)
  3. Newsgroups: sci.logic
  4. Subject: Re: Types of type theory (Errata)
  5. Message-ID: <ALTI.92Nov16224220@tanera.dcs.ed.ac.uk>
  6. Date: 16 Nov 92 22:42:20 GMT
  7. References: <BxIxGz.D7x@access.digex.com> <1992Nov12.144654.7493@ucthpx.uct.ac.za>
  8.     <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
  9.     <1992Nov13.123046.17412@husc3.harvard.edu>
  10.     <ALTI.92Nov16194749@tanera.dcs.ed.ac.uk>
  11. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  12. Organization: LFCS, Edinburgh
  13. Lines: 19
  14. In-Reply-To: alti@dcs.ed.ac.uk's message of Mon, 16 Nov 1992 19:47:49 GMT
  15.  
  16. In article <ALTI.92Nov16194749@tanera.dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:
  17.  
  18.    Certainly, but this just means that you have to give up something to
  19.    get classical reasoning AND propositions as types. I am not an expert
  20.    in this area but as I understand it: You may have a computational
  21.    interpretation of type theory if you 'fix' your evaluation strategy
  22.              ^^^^^^^^^^^
  23. Should read: classical logic
  24.  
  25.    (i.e. you decide to use only the equations of the call-by-value
  26.    \lambda calculus). 
  27.  
  28. Sorry.
  29. --
  30.  
  31.  Thorsten Altenkirch             And there's a hand, my trusty fiere,
  32.  Laboratory for Foundations         And gie's a hand o' thine,
  33.  of Computer Science               And we'll tak a right guid-willie waught
  34.  University of Edinburgh            For auld lang syne!
  35.