Lambda the Ultimate

inactiveTopic Constructive Computation Theory. Course notes on lambda calculus
started 6/29/2003; 12:54:45 AM - last post 6/29/2003; 10:40:29 AM
Ehud Lamm - Constructive Computation Theory. Course notes on lambda calculus  blueArrow
6/29/2003; 12:54:45 AM (reads: 1223, responses: 1)
Constructive Computation Theory. Course notes on lambda calculus
G. Huet. Constructive Computation Theory. Course notes on lambda calculus, University of Bordeaux I, 2002.

We give in these notes an overview of computation theory, presented in the paradigm of - calculus. The descriptive formalism used is not the usual meta-language of Mathematics, but an actual programming language, Pidgin ML, a variant of Objective Caml, developed in IN- RIA Rocquencourt. This has the double advantage of being more rigorous, more constructive, and of allowing better understanding by the reader who may interactively execute all definitions and examples of the course. The corresponding programs may be downloaded from the site http://pauillac.inria.fr/~huet/FREE/LAMBDA.tar.gz. The programs may be executed with Objective Caml, version 3.06 (http://caml.inria.fr/ocaml/index.html).

I found the link to these nice lecture notes in a TYPES messages, in regard to Mitch Wand's request for teaching materials for a freshmen honors seminar, in which he wants to take a look at computability theory, using lambda-calculus as a vehicle.

As LtU regulars know, I am a firm believer in using constructive methods in introductory computer science. But at the moment, Haskell is the language that gets my vote not O'caml...


Posted to LC by Ehud Lamm on 6/29/03; 1:03:00 AM

Jim Apple - Re: Constructive Computation Theory. Course notes on lambda calculus  blueArrow
6/29/2003; 10:40:29 AM (reads: 448, responses: 0)
The new web page can be found at http://pauillac.inria.fr/~huet/CCT/ The programs are available at http://pauillac.inria.fr/~huet/CCT/cct.tar.gz