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.

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.