Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In ICFP 2002: International Conference on Functional Programming, pages 235--246. ACM, 2002.

Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and β-equivalence checker for the λ-calculus with products, sums, and guarded fixpoints. Our approach is based on compilation to the bytecode of an abstract machine performing weak reductions on non-closed terms, derived with minimal modifications from the ZAM machine used in the Objective Caml bytecode interpreter, and complemented by a recursive “read back” procedure. An implementation in the Coq proof assistant demonstrates important speed-ups compared with the original interpreter-based implementation of strong reduction in Coq.

bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.