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 metalanguage 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
lambdacalculus 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

