# 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.

Gerard.Huet@inria.fr
Last update : August 11th, 2011