Skip to Main content Skip to Navigation
Conference papers

A Compiled Implementation of Strong Reduction

Benjamin Grégoire 1 Xavier Leroy 2
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, April 1, 2017 - 5:38:55 PM
Last modification on : Thursday, June 17, 2021 - 3:46:15 AM
Long-term archiving on: : Sunday, July 2, 2017 - 12:40:16 PM


Files produced by the author(s)



Benjamin Grégoire, Xavier Leroy. A Compiled Implementation of Strong Reduction. ICFP '02: seventh ACM SIGPLAN international conference on Functional programming , ACM, Oct 2002, Pittsburgh, United States. pp.235-246, ⟨10.1145/581478.581501⟩. ⟨hal-01499941⟩



Record views


Files downloads