Sciweavers

ICFP
2002
ACM

A compiled implementation of strong reduction

14 years 3 months ago
A compiled implementation of strong reduction
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 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 speedups compared with the original interpreter-based implementation of strong reduction in Coq. Categories and Subject Descriptors D.3.1 [Programming Languages]: Language Classifications-applicative (functional) languages; D.3.4 [Programming Languages]: Processors--compilers, interpreters; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages--operational semantics, partial evaluation; F.4.1 [Mathematical Logic and ...
Benjamin Grégoire, Xavier Leroy
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2002
Where ICFP
Authors Benjamin Grégoire, Xavier Leroy
Comments (0)