Constructive Computation Theory

This is the distribution site of the course on Constructive Computation Theory developed by Gérard Huet at INRIA at the Rocquencourt laboratory.

This is an executable course, implemented in Pidgin ML, which is a core subset of the Objective Caml programming language under the so-called revised syntax.

A previous version of these notes in French was circulated between 1988 and 1991 under the name: "Initiation au lambda-calcul". It formed the notes of a graduate course for the "DEA d'Informatique Fondamentale" at Université Paris VII. The next version formed the lambda-calculus portion of a course on Functional Programming given by the author at the Computer Science Division of AIT, Bangkok (Thailand), in 1992. The support of AIT is gratefully acknowledged. An update was prepared for the "Ecole Jeunes Chercheurs du Greco de Programmation'', Bordeaux, April 1992, and revised as notes for a course on lambda-calculus for the DEA Informatique, Mathématiques et Applications, taught at ENS in Paris during Fall 1992 and 1993, and for the DEA Fonctionnalité et Théorie des Types, Université Paris 7 in 1994. This course was taught again in the DEA d'Informatique de l'Universit\'e Bordeaux I in 2002. This course was last taught at the MPRI (Master Parisien de Recherche en Informatique) in Paris in 2004, in the course "Calculs Algébriques et Fonctionnels".

The author is grateful for any comment/criticism of this work, which may be communicated by electronic mail here.

A compressed tar file is available. Under Unix/Linux/MacOSX, untarring this file will yield all sources in a directory CCT, and a README file which provides installation information. Enjoy!

The courses notes - which contain the documentation of the software in literate programming style, are available as CCT.pdf.
Last update : August 11th, 2011