Efficient Reduction in Coq

• Abstract and slides of the talk given at the Department of Artificial Intelligence in Ulm on June 98. DVI, Postscript,
• The OCaml sources of the implementation of a few reduction functions including the KAM, KN abstract machines.Download the sources.