Abstract of the talk

This talk is about the implementation of efficient reduction functions in the framework of proof-checkers in which proofs and programs are represented by lambda-terms. The goal is to compute normal forms (or reducts) of such lambda-terms.

The necessity of computing efficiently appears at least in two cases:

Implementing the reduction following the formal definition of beta-reduction is very inefficient. An important improvement as been carried out by Krivine's Abstract Machine (KAM), which uses the notion of closure. In his PhD thesis, Pierre Crégut derived new abstract machines, allowing the reduction of terms with free variables, and using a lazy strategy.

In the talk, I will explain the general ideas that lead the design of the new reduction functions in the Coq proof-assistant. Some examples of ML programs will illustrate these ideas. The technical part will consist of the introduction of a calculus with closures (seen as a restriction of explicit substitutions), from which an abstract machine can be directly implemented.