Lambda the Ultimate

Proofs and Types
started 10/7/2003; 11:29:19 AM - last post 10/17/2003; 12:16:21 PM

Ehud Lamm - Proofs and Types

10/7/2003; 11:29:19 AM (reads: 8665, responses: 4)

Proofs and Types

(vai Frank, in the discussion group)

Proofs and Types by Jean-Yves Girard, translated and with appendices by Yves Lafont and Paul Taylor, 1989.

Based on a short graduate course on typed lambda-calculus given at the Université Paris VII in the autumn term of 1986-7.

An very interesting book that has gone out of print and is now available online.

A taste of the topics discussed in this smorgasbord: The Curry-Howard Isomorphism, Strong Normalisation, System F, Provably Total Functions and more!

Posted to theory by Ehud Lamm on 10/7/03; 11:30:26 AM

Frank Atanassow - Re: Proofs and Types

10/9/2003; 5:33:13 AM (reads: 401, responses: 0)

Here's another recent addition to PLT Online:

David E. Rydeheard and Rod M. Burstall. Computational Category Theory. (link)

Ehud Lamm - Re: Proofs and Types

10/9/2003; 6:10:46 AM (reads: 400, responses: 0)

What the book really lacks is exercises (hopefully with solutions). I wonder if there are courses based on the book with online assignments.

Neel Krishnaswami - Re: Proofs and Types

10/10/2003; 5:56:53 PM (reads: 355, responses: 0)

Girard (or at least, his translators) has a really excellent prose style.

Darius Bacon - Re: Proofs and Types

10/17/2003; 12:16:21 PM (reads: 238, responses: 0)

Thanks for posting this -- that book's been on my to-read list for years.