A Compiled Implementation of Strong Reduction - Archive ouverte HAL Access content directly
Conference Papers Year :

A Compiled Implementation of Strong Reduction

(1) , (2)
1
2
Benjamin Grégoire

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.
Fichier principal
Vignette du fichier
strong-reduction.pdf (121.95 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01499941 , version 1 (01-04-2017)

Identifiers

Cite

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⟩
287 View
349 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More