Benjamin Grégoire
Xavier Leroy
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.
- A. W. Appel. Compiling with continuations. Cambridge University Press, 1992.]] Google Scholar
Digital Library
- K. Appel and W. Haken. Every planar map is four colorable. Illinois J. Math, 21:429--567, 1977.]]Google ScholarCross Ref
- B. Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, University Paris~7, 1999.]]Google Scholar
- B. Barras. Programming and computing in HOL. In Theorem Proving in Higher Order Logics 2000, volume 1869 of LNCS, pages 17--37. Springer-Verlag, 2000.]] Google ScholarDigital Library
- B. Barras and B. Werner. Coq in Coq. Submitted for publication, 2000.]]Google Scholar
- U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Logic in Computer Science '91, pages 203--211. IEEE Computer Society Press, 1991.]]Google ScholarCross Ref
- T. Coquand and G. Huet. The calculus of Constructions. Inf. and Comp., 76(2/3):95--120, 1988.]] Google ScholarDigital Library
- G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. Science of Computer Programming, 8(2):173--202, 1987.]] Google ScholarDigital Library
- P. Crégut. An abstract machine for lambda-terms normalization. In Lisp and Functional Programming 1990, pages 333--340. ACM Press, 1990.]] Google ScholarDigital Library
- P. Crégut. Machines à environnement pour la réduction symbolique et l'évaluation partielle. PhD thesis, University Paris 7, 1991.]]Google Scholar
- O. Danvy. Type-directed partial evaluation. In 23rd symp. Principles of Progr. Lang, pages 242--257. ACM Press, 1996.]] Google ScholarDigital Library
- O. Danvy. Online type-directed partial evaluation. Technical Report RS-97-53, BRICS, 1997.]]Google ScholarCross Ref
- T. Hardin, L. Maranget, and B. Pagano. Functional runtimes within the lambda-sigma calculus. Journal of Functional Programming, 8(2):131--176, 1998.]] Google ScholarDigital Library
- R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143--184, 1993.]] Google ScholarDigital Library
- N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.]] Google ScholarDigital Library
- X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990.]]Google Scholar
- X. Leroy, D. Doligez, J. Garrigue, and J. Vouillon. The Objective Caml system. Software and documentation available on the Web Logiciel et documentation disponibles sur le Web, http://caml.inria.fr/, 1996--2002.]]Google Scholar
- A. Miquel. Le Calcul des Constructions implicite: syntaxe et sémantique. PhD thesis, University Paris 7, 2001.]]Google Scholar
- G. Nadathur and D. S. Wilson. A notation for lambda terms: A generalization of environments. Theoretical Comput. Sci., 198:49--98, 1998.]] Google ScholarDigital Library
- S. L. Peyton Jones. Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. Journal of Functional Programming, 2(2):127--202, 1992.]]Google ScholarCross Ref
- F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Mathematical Foundations of Programming Semantics, volume 442 of LNCS, pages 209--228. Springer-Verlag, 1990.]] Google ScholarDigital Library
- E. Sumii and N. Kobayashi. Online type-directed partial evaluation for dynamically-typed languages. Computer Software, 17(3):38--62, 2000. Iwanami Shoten.]]Google Scholar
- K. N. Verma, J. Goubault-Larrecq, S. Prasad, and S. Arun-Kumar. Reflecting BDDs in Coq. In 6th Asian Computing Science Conference (ASIAN'2000), number 1961 in LNCS, pages 162--181. Springer-Verlag, 2000.]] Google ScholarDigital Library
- R. Vestergaard. The polymorphic type theory of normalisation by evaluation. Draft, 2001.]]Google Scholar
Index Terms
- A compiled implementation of strong reduction
Recommendations
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 ...
Strong Reduction of Combinatory Calculus with Streams
This paper gives the strong reduction of the combinatory calculus SCL, which was introduced as a combinatory calculus corresponding to the untyped Lambda-mu calculus. It proves the confluence of the strong reduction. By the confluence, it also proves ...
Formalizing Type Operations Using the “Image” Type Constructor
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Comments