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:

when using the reflection technique, which consists mainly of doing a proof by computation (given a theorem stating that the computation is sound)
if we consider the proof-checker as a programming language, that is proving properties and executing programs in the same environment.

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.