A compiled implementation of strong reduction
In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP'02)ACM SIGPLAN notices 37(9):235-246; Jg. 37 (2002) 9, S. 235-246
Konferenz
- print, 24 ref
Zugriff:
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.
Titel: |
A compiled implementation of strong reduction
|
---|---|
Autor/in / Beteiligte Person: | GREGOIRE, Benjamin ; LEROY, Xavier |
Link: | |
Quelle: | Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP'02)ACM SIGPLAN notices 37(9):235-246; Jg. 37 (2002) 9, S. 235-246 |
Veröffentlichung: | Broadway, NY: ACM, 2002 |
Medientyp: | Konferenz |
Umfang: | print, 24 ref |
ISSN: | 1523-2867 (print) |
Schlagwort: |
|
Sonstiges: |
|