A proof theory for generic judgments

ABSTRACT

The operational semantics of a computation system is often presented as inference rules or, equivalently, as logical theories. Specifications can be made more declarative and high level if syntactic details concerning bound variables and substitutions are encoded directly into the logic using term-level abstractions (λ-abstraction) and proof-level abstractions (eigenvariables). When one wishes to use such logical theories to support reasoning about properties of computation, the usual quantifiers and proof-level abstractions do not seem adequate: proof-level abstraction of variables with scope over sequents (global scope) as well as over only formulas (local scope) seem required for many examples. We will present a sequent calculus that provides this local notion of proof-level abstraction via generic judgment and a new quantifier, ∇, which explicitly manipulates such local scope. Intuitionistic logic extended with ∇ satisfies cut-elimination even when the logic is additionally strengthened with a proof theoretic notion of definitions. The resulting logic can be used to encode naturally a number of examples involving abstractions, and we illustrate the uses of ∇ with the π-calculus and an encoding of provability of an object-logic.

REFERENCES

• 1: I. Cervesato , N. A. Durgin , P. D. Lincoln , J. C. Mitchell , A. Scedrov, A Meta-Notation for Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.55, June 28-30, 1999
• 2: Iliano Cervesato , Frank Pfenning, A Linear Logical Framework, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.264, July 27-30, 1996
• 3: Jawahar Lal Chirimar, Proof theoretic approach to specification languages, University of Pennsylvania, Philadelphia, PA, 1995
• 4: Church, A. 1940. A formulation of the simple theory of types. J. Symbol. Logic 5, 56--68.
• 5: Lars-Henrik Eriksson, A Finitary Version of the Calculus of Partial Inductive Defintions, Proceedings of the Second International Workshop on Extensions of Logic Programming, p.89-134, January 27-29, 1991
• 6: Amy P. Felty , Dale Miller, Specifying Theorem Provers in a Higher-Order Logic Programming Language, Proceedings of the 9th International Conference on Automated Deduction, p.61-80, May 23-26, 1988
• 7: Murdoch Gabbay , James Cheney, A Sequent Calculus for Nominal Logic, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.139-148, July 13-17, 2004 [doi>10.1109/LICS.2004.6]
• 8: Gabbay, M. J. and Pitts, A. M. 2001. A new approach to abstract syntax with variable binding. Form. Aspects Comput. 13, 341--363.
• 9: Gentzen, G. 1969. Investigations into logical deductions. In The Collected Papers of Gerhard Gentzen, M. E. Szabo, Ed. North-Holland Publishing Co., Amsterdam, The Netherlands, 68-- 131.
• 10: Girard, J.-Y. 1992. A fixpoint theorem in linear logic. Email to the [e-mail] mailing list.
• 11: Hallnäs, L. and Schroeder-Heister, P. 1991. A proof-theoretic approach to logic programming. II. Programs as definitions. J. Logic Comput. 1, 5 (Oct.), 635--660.
• 12: Huet, G. 1975. A unification algorithm for typed λ-calculus. Theoret. Comput. Sci. 1, 27--57.
• 13: Raymond Charles Mcdowell , Dale Miller, Reasoning in a logic with definitions and induction, 1997
• 14: Raymond McDowell , Dale Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, v.232 n.1-2, p.91-11,9, Feb. 6, 2000 [doi>10.1016/S0304-3975(99)00171-1]
• 15: Raymond C. McDowell , Dale A. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic (TOCL), v.3 n.1, p.80-136, January 2002 [doi>10.1145/504077.504080]
• 16: Raymond McDowell , Dale Miller , Catuscia Palamidessi, Encoding transition systems in sequent calculus, Theoretical Computer Science, v.294 n.3, p.411-437, 18 February 2003 [doi>10.1016/S0304-3975(01)00168-2]
• 17: Miller, D. 1989. Lexical scoping as universal quantification. In Proceedings of the 6th International Logic Programming Conference (Lisbon, Portugal). MIT Press, Cambridge, MA, 268--283.
• 18: Miller, D. 1991. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput. 1, 4, 497--536.
• 19: Dale Miller, Unification under a mixed prefix, Journal of Symbolic Computation, v.14 n.4, p.321-358, Oct. 1992 [doi>10.1016/0747-7171(92)90011-R]
• 20: Dale Miller, The pi-Calculus as a Theory in Linear Logic: Preliminary Results, Proceedings of the Third International Workshop on Extensions of Logic Programming, p.242-264, February 26-28, 1992
• 21: Dale Miller, Forum: a multiple-conclusion specification logic, Theoretical Computer Science, v.165 n.1, p.201-232, Sept. 30, 1996
• 22: Dale Miller, Abstract Syntax for Variable Binders: An Overview, Proceedings of the First International Conference on Computational Logic, p.239-253, July 01, 2000
• 23: Miller, D. and Palamidessi, C. 1999. Foundational aspects of syntax. In ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, and P. Wegner, Eds. Vol. 31. ACM, New York.
• 24: Dale Miller , Alwen Fernanto Tiu, Encoding Generic Judgments, Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, p.18-32, December 12-14, 2002
• 25: Dale Miller , Alwen Tiu, A Proof Theory for Generic Judgments: An extended abstract, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.118, June 22-25, 2003
• 26: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 27: Momigliano, A., Ambler, S., and Crole, R. 2002. A hybrid encoding of Howe's method for establishing congruence of bisimilarity. In LFM'02. ENTCS, vol. 70.2. Springer-Verlag, New York.
• 28: Momigliano, A. and Tiu, A. 2003. Induction and co-induction in sequent calculus. In Proceedings of TYPES 2003 Workshop. Lecture Notes in Computer Science, vol. 3085, Springer-Verlag, New York, 293--308.
• 29: Nipkow, T. 1993. Functional unification of higher-order patterns. In Proceedings of the 8th IEEE Symposium on Logic in Computer Science (LICS 1993), M. Vardi, Ed. IEEE Computer Society Press, Los Alamitos, CA, 64--74.
• 30: L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, v.5 n.3, p.363-397, September 1989 [doi>10.1007/BF00248324]
• 31: 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
• 32: Frank Pfenning , Ekkehard Rohwedder, Implementing the Meta-Theory of Deductive Systems, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.537-551, June 15-18, 1992
• 33: 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]
• 34: Peter Schroeder-Heister, Cut Elimination for Logics with Definitional Reflection, Proceedings of the International Workshop on Nonclassical Logics and Information Processing, p.146-171, November 09-10, 1992
• 35: Schroeder-Heister, P. 1994. Cut elimination for logics with definitional reflection and restricted initial sequents. In Proceedings of the Post-Conference Workshop of ICLP 1994 on Proof-Theoretic Extensions of Logic Programming.
• 36: Schürmann, C. 2000. Automating the meta theory of deductive systems. Ph.D. dissertation, Carnegie Mellon University.
• 37: Slaney, J. 1989. Solution to a problem of Ono and Komori. J. Philosophic Logic 18, 103--111.
• 38: Tiu, A. 2004a. Level 0/1 prover: A tutorial. Available via the web and from Tiu.
• 39: Alwen F. Tiu , John Hannan, A logical framework for reasoning about logical specifications, 2004
• 40: Tiu, A. and Miller, D. 2004. A proof search specification of the π-calculus. In Proceedings of the 3rd Workshop on the Foundations of Global Ubiquitous Computing.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Design, Theory, Verification

Keywords:
λ-tree syntax, ∇-quantifier, Proof search, generic judgments, higher-order abstract syntax, reasoning about operational semantics