Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

ABSTRACT

We investigate the development of a general-purpose framework for mechanized reasoning about the meta-theory of programming languages. In order to provide a standard, uniform account of a programming language, we propose to define it as a logic in a logical framework, using the same mechanisms for definition, reasoning, and automation that are available to other logics. Then, in order to reason about the language's meta-theory, we use reflection to inject the programming language into (usually richer and more expressive) meta-theory.One of the key features of our approach is that structure of the language is preserved when it is reflected, including variables, meta-variables, and binding structure. This allows the structure of proofs to be preserved as well, and there is a one-to-one map from proof steps in the original programming logic to proof steps in the reflected logic. The act of reflecting a language is automated; all definitions, theorems, and proofs are preserved by the transformation and all the key lemmas (such as proof and structural induction) are automatically derived.The principal representation used by the reflected logic is higher-order abstract syntax (HOAS). However, reasoning about terms in HOAS can be awkward in some cases, especially for variables. For this reason, we define a computationally equivalent variable-free de Bruijn representation that is interchangeable with the HOAS in all contexts. The de Bruijn representation inherits the properties of substitution and alpha-equality from the logical framework, and it is not complicated by administrative issues like variable renumbering.We further develop the concepts and principles of proofs, provability, and structural and proof induction. This work is fully implemented in the MetaPRL theorem prover. We illustrate with an application to F<: as defined in the POPLmark challenge.

REFERENCES

• 1: William Aitken and Robert L. Constable. Reflecting on NuPRL: Lessons 1-4. Technical report, Cornell University, Computer Science Department, Ithaca, NY, 1992.
• 2: William E. Aitken , Robert L. Constable , Judith L. Underwood, Metalogical Frameworks II: Developing a Reflected Decision Procedure, Journal of Automated Reasoning, v.22 n.2, p.171-221, February 1999 [doi>10.1023/A:1005929703675]
• 3: Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The semantics of reflected proof. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 95--197. IEEE Computer Society Press, June 1990.
• 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. Available from http://www.cis.upenn.edu/group/proj/plclub/mmm/,2005.
• 5: James Cheney, Toward a general theory of names: binding and scope, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.33-40, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088454.1088459]
• 6: Robert L. Constable. Using reflection to explain and enhance type theory. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO Series F, pages 65--100. Springer, Berlin, 1994.
• 7: N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagaciones Mathematische, 34:381--392, 1972. This also appeared in the Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam, series A, 75, No. 5.
• 8: Kurt Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme I. Monatshefte für Mathematik und Physik, 38:173--198, 1931. English version in {24}.
• 9: 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]
• 10: J. Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-53, SRI International, Cambridge Computer Science Research Centre, Millers Yard, Cambridge, UK, February 1995.
• 11: Dimitri Hendriks, Proof Reflection in Coq, Journal of Automated Reasoning, v.29 n.3-4, p.277-307, 2002 [doi>10.1023/A:1021923116629]
• 12: Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL-A modular logical environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2003
• 13: Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov. Practical reflection for sequent logics. In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Electronic Notes in Theoretical Computer Science, 2006. To appear.
• 14: Jason J. Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, and Xin Yu. A listing of MetaPRL theories. http://metaprl.org/theories.pdf.
• 15: Jason J. Hickey, Aleksey Nogin, Alexei Kopylov, et al. MetaPRL home page. http://metaprl.org/.
• 16: Aleksey Nogin , Jason Hickey, Sequent Schema for Derived Rules, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.281-297, August 20-23, 2002
• 17: Aleksey Nogin and Alexei Kopylov. Formalizing type operations using the "Image" type constructor. Accepted to to Workshop on Logic, Language, Information and Computation (WoLLIC), 2006.
• 18: Aleksey Nogin , Alexei Kopylov , Xin Yu , Jason Hickey, A computational approach to reflective meta-reasoning about languages with bindings, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.2-12, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088454.1088456]
• 19: Russell OConnor. Essential incompleteness of arithmetic verified by Coq. InProceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), volume 3603 of Lecture Notes in Computer Science, pages 245--260, 2005.
• 20: 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
• 21: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 22: Gordon Plotkin. An illative theory of relations. In R. Cooper, K. Mukai, and J. Perry, editors, Situation Theory and Its Applications, Volume 1, number 22 in CSLI Lecture Notes, pages 133--146. Centre for the Study of Language and Information, 1990.
• 23: Harald Rueß, Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.319-335, April 02-04, 1997
• 24: J. van Heijenoort, editor. From Frege to Gödel: A Source Book in Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 1967.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Operations on languages

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

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

General Terms:
Languages, Theory, Verification

Keywords:
higher-order abstract syntax, languages with bindings, mechanized reasoning, meta-theory, metaPRL, nuPRL, reflection, type theory