Reasoning with hypothetical judgments and open terms in hybrid

ABSTRACT

Hybrid is a system developed to specify and reason about logics, programming languages, and other formal systems expressed in higher-order abstract syntax (HOAS). An important goal of Hybrid is to exploit the advantages of HOAS within the well-understood setting of higher-order logic as implemented by systems such as Isabelle and Coq. In this paper, we add new capabilities for reasoning by induction on encodings of object-level inference rules. Elegant and succinct specifications of such inference rules can often be given using hypothetical and parametric judgments, which are represented by embedded implication and universal quantification. Induction over such judgments is well-known to be problematic. In previous work, we showed how to express this kind of judgment using a two-level approach, but reasoning by induction on such judgments was restricted to closed terms. The new capabilities we add include techniques for adding arbitrary "new" variables to contexts and inductively reasoning about open terms. Very little overhead is required, namely a small library of definitions and lemmas, yet the reasoning power of the system and the class of properties that can be proved is significantly increased. We illustrate the approach using PCF, a simple programming language that serves as the core of a variety of functional languages. We encode the typing judgment, and prove by induction on this judgment that well-typed PCF terms have unique types.

REFERENCES

• 1: Simon Ambler, Roy L. Crole, and Alberto Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In Carreño et al. [2002], pages 13--30.
• 2: 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, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 50--65. Springer, 2005.
• 3: Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, 2004.
• 4: Victor Carreño, César Muñoz, and Sofiène Tashar, editors. 15th International Conference on Theorem Proving in Higher Order Logics, volume 2410 of Lecture Notes in Computer Science, 2002. Springer.
• 5: Joëlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In 2nd International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 124--138. Springer, 1995.
• 6: Lars-Henrik Eriksson. Pi: an interactive derivation editor for the calculus of partial inductive definitions. In Alan Bundy, editor, 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science, pages 821--825. Springer, 1994.
• 7: Amy P. Felty. Two-level meta-reasoning in Coq. In Carreño et al. [2002], pages 198--213.
• 8: Amy P. Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. CoRR, abs/0811.4367, 2008.
• 9: Andrew Gacek. The Abella interactive theorem prover (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, 4th International Joint Conference on Automated Reasoning, volume 5195 of Lecture Notes in Computer Science, pages 154--161. Springer, 2008.
• 10: Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In 23rd Annual IEEE Symposium on Logic in Computer Science, pages 33--44. IEEE Computer Society, 2008.
• 11: Elsa L. Gunter. Why we can't have SML-style datatype declarations in HOL. In Luc J.M. Claesen and Michael J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20, pages 561--568. North-Holland/Elsevier, 1992.
• 12: Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. J. Funct. Program., 17 (4-5): 613--673, 2007.
• 13: Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, 28th International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 963--978. Springer, 2001.
• 14: Hybrid Group. Hybrid: A package for higher-order syntax in Isabelle and Coq. www.hybrid.dsi.unimi.it, 2009.
• 15: Raymond McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, 1997.
• 16: Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log., 3 (1): 80--136, January 2002.
• 17: James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reasoning, 23 (3-4): 373--409, 1999.
• 18: Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. Comput. Logic, 6 (4): 749--783, 2005.
• 19: Dale Miller and Alwen Fernanto Tiu. Encoding generic judgments. In Manindra Agrawal and Anil Seth, editors, 22nd Conference on Foundations of Software Technology and Theoretical Computer Science, volume 2556 of Lecture Notes in Computer Science, pages 18--32. Springer, 2002.
• 20: Alberto Momigliano and Alwen Fernanto Tiu. Induction and co-induction in sequent calculus. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, International Workshop, TYPES 2003, Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science, pages 293--308. Springer, 2003.
• 21: Alberto Momigliano, Alan J. Martin, and Amy P. Felty. Two-level Hybrid: A system for reasoning using higher-order abstract syntax. Electr. Notes Theor. Comput. Sci., 196: 85--93, 2008.
• 22: Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of phLecture Notes in Computer Science. Springer, 2002.
• 23: Nominal Methods Group. Nominal Isabelle. isabelle.in.tum.de/nominal/, 2009.
• 24: Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In M. Bezem and J.F. Groote, editors, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 328--345. Springer, 1993.
• 25: Lawrence C. Paulson. A fixed point approach to implementing (co)inductive definitions. In Alan Bundy, editor, 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science, pages 148--161. Springer, 1994.
• 26: Frank Pfenning and Carsten Schürmann. System description: Twelf -- a meta-logical framework for deductive systems. In H. Ganzinger, editor, 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Computer Science, pages 202--206. Springer, 1999.
• 27: Brigitte Pientka. Verifying termination and reduction properties about higher-order logic programs. J. Autom. Reasoning, 34 (2): 179--207, 2005.
• 28: Brigitte Pientka. Proof pearl: The power of higher-order encodings in the logical framework lf. In Klaus Schneider and Jens Brandt, editors, 20th International Conference on Theorem Proving in Higher Order Logics, volume 4732 of Lecture Notes in Computer Science, pages 246--261. Springer, 2007.
• 29: Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186 (2): 165--193, 2003.
• 30: Carsten Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. CMU-CS-00-146.
• 31: Carsten Schürmann. A type-theoretic approach to induction with higher-order encodings. In Robert Nieuwenhuis and Andrei Voronkov, editors, 8th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, volume 2250 of Lecture Notes in Computer Science, pages 266--281. Springer, 2001.
• 32: Carsten Schürmann and Frank Pfenning. A coverage checking algorithm for LF. In David A. Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics, volume 2758 of Lecture Notes in Computer Science, pages 120--135. Springer, 2003.
• 33: Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theor. Comput. Sci., 121 (1-2): 411--440, 1993. http://dx.doi.org/10.1016/0304-3975(93)90095-B.
• 34: Alwen Tiu. A logic for reasoning about generic judgments. Electr. Notes Theor. Comput. Sci., 174 (5): 3--18, 2007.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Lambda calculus and related systems; Mechanical theorem proving

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Metatheory**; Logic programming; Inference engines

General Terms:
Languages, Verification

Keywords:
higher-order abstract syntax, induction, interactive theorem proving, logical frameworks, name-binding