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