Engineering formal metatheory

ABSTRACT

Machine-checked proofs of properties of programming languages have become acritical need, both for increased confidence in large and complex designsand as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. There presentation and manipulation of terms with variable binding is a key issue.

We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductivedefinitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over other methodologies using first-order representations, leading to developments that are faithful to informal practice, yet require noexternal tool support and little infrastructure within the proof assistant.

We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F sub; and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension.

REFERENCES

• 1: Thorsten Altenkirch, A Formalization of the Strong Normalization Proof for System F in LEGO, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.13-28, March 16-18, 1993
• 2: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 3: Michael Ashley-Rollman, Karl Crary, and Robert Harper. Submission to the POPLMARK challenge. Available from http://www.cis.upenn.edu/~plclub/mmm/, 2005.
• 4: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLMARK challenge. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, volume 3603 of Lecture Notes in Computer Science, pages 50--65. Springer, 2005.
• 5: Henk P. Barendregt. The Lambda Calculus. North Holland, revised edition, 1984.
• 6: Bruno Barras and Benjamin Werner. Coq in coq. Available from http://pauillac.inria.fr/~barras/coq_work-eng.html, 1997.
• 7: Proceedings of the International Conference on Typed Lambda Calculi and Applications, March 1993
• 8: Anna Bucalo , Furio Honsell , Marino Miculan , Ivan Scagnetto , Martin Hoffman, Consistency of the theory of contexts, Journal of Functional Programming, v.16 n.3, p.327-395, May 2006 [doi>10.1017/S0956796806005892]
• 9: Adam Chlipala. Submission to the POPLMARK challenge, part 1a. Available from http://www.cs.berkeley.edu/~adamc/poplmark/, 2006.
• 10: The Coq Development Team. The Coq proof assistant reference manual, version 8.1. Available from http://coq.inria.fr/, 2007.
• 11: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 12: Karl Crary, Toward a foundational typed assembly language, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.198-212, January 15-17, 2003, New Orleans, Louisiana, USA
• 13: N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381--392, 1972.
• 14: Joëlle Despeyroux , Amy P. Felty , André Hirschowitz, Higher-Order Abstract Syntax in Coq, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.124-138, April 10-12, 1995
• 15: Peter Dybjer. Inductive families. Formal Aspects of Computing, 6:1--26, 1994.
• 16: Jonathan M. Ford and Ian A. Mason. Operational techniques in PVS - A preliminary evaluation. Electronic Notes in Theoretical Computer Science, 42, 2001.
• 17: Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, 1969. Edited by Mandred Szabo.
• 18: Andrew D. Gordon, A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.413-425, August 11-13, 1993
• 19: Andrew D. Gordon , Thomas F. Melham, Five Axioms of Alpha-Conversion, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.173-190, August 26-30, 1996
• 20: ROBERT HARPER , DANIEL R. LICATA, Mechanizing metatheory in a logical framework, Journal of Functional Programming, v.17 n.4-5, p.613-673, July 2007 [doi>10.1017/S0956796807006430]
• 21: 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]
• 22: Dimitri Hendriks and Vincent van Oostrom. Adbmal. In F. Baader, editor, Automated Deduction - CADE-19, volume 2741 of Lecture Notes in Artificial Intelligence, pages 136--150. Springer-Verlag, 2003.
• 23: Peter Homeier. A proof of the Church-Rosser theorem for the lambda calculus in higher order logic. In Richard J. Boulton and Paul B. Jackson, editors, TPHOLs 2001: Supplemental Proceedings, pages 207--222. Division of Informatics, University of Edinburgh, September 2001. Available as Informatics Research Report EDI-INF-RR-0046.
• 24: Furio Honsell, Marino Miculan, and Ivan Scagnetto. The theory of contexts for first order and higher order abstract syntax. Electronic Notes in Theoretical Computer Science, 62, 2002.
• 25: Gérard Huet. The constructive engine. In Raghavan Narasimhan, editor, A Perspective in Theoretical Computer Science: Commerative Volume for Gift Siromoney. World Scientific Publishing, 1989. Also available as INRIA Technical Report 110.
• 26: Gérard Huet. Residual theory inall-calculus: A formal development. Journal of Functional Programming, 4(3):371--394, July 1994. Also available as INRIA Research Report 2009 (August 1993).
• 27: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 28: J. L. Krivine, Lambda-calculus, types and models, Ellis Horwood, Upper Saddle River, NJ, 1993
• 29: Daniel K. Lee , Karl Crary , Robert Harper, Towards a mechanized metatheory of standard ML, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 30: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 31: Xavier Leroy. A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA, January 2007.
• 32: Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.
• 33: Conor McBride , James McKinna, Functional pearl: i am not a number--i am a free variable, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017477]
• 34: James McKinna , Robert Pollack, Pure Type Systems Formalized, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.289-305, March 16-18, 1993
• 35: James Mckinna , Robert Pollack, Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, v.23 n.3, p.373-409, November 1999 [doi>10.1023/A:1006294005493]
• 36: Tobias Nipkow, More Church–Rosser Proofs, Journal of Automated Reasoning, v.26 n.1, p.51-66, January 2001 [doi>10.1023/A:1006496715975]
• 37: Michael Norrish and Konrad Slind. HOL 4. Available from http://hol.sourceforge.net/, 2007.
• 38: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 39: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 40: Andrew M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, v.186 n.2, p.165-193, 01 November 2003 [doi>10.1016/S0890-5401(03)00138-X]
• 41: Randy Pollack. Reasoning about languages with binding: Can we do it yet?, February 2006. Presentation, slides available from http://homepages.inf.ed.ac.uk/rpollack/.
• 42: Randy Pollack, Closure under alpha-conversion, Proceedings of the international workshop on Types for proofs and programs, p.313-332, January 1994, Nijmegen, The Netherlands
• 43: Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Univ. of Edinburgh, 1994b.
• 44: Dag Prawitz. Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm, 1965.
• 45: Ole Rasmussen. The Church-Rosser theorem in Isabelle: A proof porting experiment. Technical Report 364, University of Cambridge, Computer Laboratory, March 1995.
• 46: Wilmer Ricciotti. Submission to the POPLMARK challenge, part 1a. Available from http://ricciott.web.cs.unibo.it/, 2007.
• 47: Peter Sewell , Francesco Zappa Nardelli , Scott Owens , Gilles Peskine , Thomas Ridge , Susmit Sarkar , Rok Strniša, Ott: effective tool support for the working semanticist, Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 48: N. Shankar, A mechanical proof of the Church-Rosser theorem, Journal of the ACM (JACM), v.35 n.3, p.475-522, July 1988 [doi>10.1145/44483.44484]
• 49: Allen Stoughton, Substitution revisited, Theoretical Computer Science, v.59 n.3, p.317-325, Aug. 1988 [doi>10.1016/0304-3975(88)90149-1]
• 50: Christian Urban, Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, v.40 n.4, p.327-356, May 2008 [doi>10.1007/s10817-008-9097-2]
• 51: Christian Urban and Randy Pollack. Locally nameless representation in Nominal Isabelle. Talk at Workshop on Mechanizing Metatheory. Available from www4.in.tum.de/~urbanc/Publications/ln.pdf, 2007.
• 52: Christian Urban, Stefan Berghofer, and Julien Narboux. Nominal datatype package for Isabelle/HOL. Available from http://isabelle.in.tum.de/nominal/, 2007a.
• 53: Christian Urban, Stefan Berghofer, and Michael Norrish. Barendregt's variable convention in rule inductions. In Proceedings of the 21th Conference on Automated Deduction (CADE 2007), volume 4603 of Lecture Notes in Computer Science, pages 35--50. Springer, 2007b.
• 54: René Vestergaard , James Brotherston, A formalised first-order confluence proof for the λ-calculus using one-sorted variable names, Information and Computation, v.183 n.2, p.212-244, 15 June 2003 [doi>10.1016/S0890-5401(03)00023-3]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

General Terms:
Design, Documentation, Languages, Theory, Verification

Keywords:
binding, coq, locally nameless