A compiled implementation of strong reduction

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.

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: K. Appel and W. Haken. Every planar map is four colorable. Illinois J. Math, 21:429--567, 1977.
• 3: B. Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, University Paris~7, 1999.
• 4: Bruno Barras, Programming and Computing in HOL, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.17-37, August 14-18, 2000
• 5: B. Barras and B. Werner. Coq in Coq. Submitted for publication, 2000.
• 6: 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.
• 7: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 8: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• 9: P. Crégut, An abstract machine for Lambda-terms normalization, Proceedings of the 1990 ACM conference on LISP and functional programming, p.333-340, June 27-29, 1990, Nice, France [doi>10.1145/91556.91681]
• 10: P. Crégut. Machines à environnement pour la réduction symbolique et l'évaluation partielle. PhD thesis, University Paris 7, 1991.
• 11: Olivier Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-257, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237784]
• 12: O. Danvy. Online type-directed partial evaluation. Technical Report RS-97-53, BRICS, 1997.
• 13: Thérèse Hardin , Luc Maranget , Bruno Pagano, Functional runtime systems within the lambda-sigma calculus, Journal of Functional Programming, v.8 n.2, p.131-176, March 1998 [doi>10.1017/S0956796898002986]
• 14: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 15: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 16: X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990.
• 17: 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.
• 18: A. Miquel. Le Calcul des Constructions implicite: syntaxe et sémantique. PhD thesis, University Paris 7, 2001.
• 19: Gopalan Nadathur , Debra Sue Wilson, A notation for lambda terms. A generalization of environment, Theoretical Computer Science, v.198 n.1-2, p.49-98, May 30, 1998 [doi>10.1016/S0304-3975(97)00184-9]
• 20: 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.
• 21: Frank Pfenning , Christine Paulin-Mohring, Inductively defined types in the calculus of constructions, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.209-226, July 1990, New Orleans, Louisiana, United States
• 22: E. Sumii and N. Kobayashi. Online type-directed partial evaluation for dynamically-typed languages. Computer Software, 17(3):38--62, 2000. Iwanami Shoten.
• 23: Kumar Neeraj Verma , Jean Goubault-Larrecq , Sanjiva Prasad , S. Arun-Kumar, Reflecting BDDs in Coq, Proceedings of the 6th Asian Computing Science Conference on Advances in Computing Science, p.162-181, November 25-27, 2000
• 24: R. Vestergaard. The polymorphic type theory of normalisation by evaluation. Draft, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Interpreters

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Partial evaluation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Lambda calculus and related systems

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Evaluation strategies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Experimentation, Languages, Theory, Verification

Keywords:
Coq, abstract machine, beta-equivalence, calculus of constructions, normalization by evaluation, strong reduction, virtual machine