|
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
|
|
Constructive Computation Theory. Course notes on lambda calculus
