Journal of Automated Reasoning

, Volume 49, Issue 2, pp 241–273

# A Two-Level Logic Approach to Reasoning About Computations

Article

## Abstract

Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called $${\cal G}$$ which represents relations over λ-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in $${\cal G}$$. We also describe an interactive theorem prover called Abella that implements $${\cal G}$$ and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations.

## Keywords

Two-level logic Nominal abstraction Generic judgments ∇-quantification λ-tree syntax

## References

1. 1.
Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: 35th ACM Symp. on Principles of Programming Languages, pp. 3–15. ACM (2008)Google Scholar
2. 2.
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the POPLmark challenge. In: Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in LNCS, pp. 50–65. Springer (2005)Google Scholar
3. 3.
Baelde, D.: A Linear Approach to the Proof-Theory of Least and Greatest Fixed Points. PhD thesis, Ecole Polytechnique (2008)Google Scholar
4. 4.
Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, pp. 391–397. Springer (2007)Google Scholar
5. 5.
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)Google Scholar
6. 6.
Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940)
7. 7.
Coquand, T., Paulin, C.: Inductively defined types. In: Conference on Computer Logic. LNCS, vol. 417, pp. 50–66. Springer (1988)Google Scholar
8. 8.
Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Second International Conference on Typed Lambda Calculi and Applications, pp. 124–138 (1995)Google Scholar
9. 9.
Felty, A., Momigliano, A.: Reasoning with hypothetical judgments and open terms in Hybrid. In: ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 83–92 (2009)Google Scholar
10. 10.
Felty, A., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. (2010). doi: Google Scholar
11. 11.
Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Fourth International Joint Conference on Automated Reasoning. LNCS, vol. 5195, pp. 154–161. Springer (2008). URL http://arxiv.org/abs/0803.2305
12. 12.
Gacek, A.: The Abella System and Homepage. http://abella.cs.umn.edu/ (2009)
13. 13.
Gacek, A.: A Framework for Specifying, Prototyping, and Reasoning About Computational Systems. PhD thesis, University of Minnesota (2009)Google Scholar
14. 14.
Gacek, A., Holte, S., Nadathur, G., Qi, X., Snow, Z.: The Teyjus System–Version 2, March 2008. Available from http://teyjus.cs.umn.edu/
15. 15.
Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48–73 (2011)
16. 16.
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)
17. 17.
Kahn, G.: Natural semantics. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 247, pp. 22–39. Springer (1987)Google Scholar
18. 18.
Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(5), 308–320 (1964)
19. 19.
Licata, D.R., Zeilberger, N., Harper, R.: Focusing on binding and computation. In: Pfenning, F. (ed.) 23th Symp. on Logic in Computer Science, pp. 241–252. IEEE Computer Society Press (2008)Google Scholar
20. 20.
McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theor. Comp. Sci. 232, 91–119 (2000)
21. 21.
McDowell, R., Miller, D. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3(1), 80–136 (2002)
22. 22.
Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358 (1992)
23. 23.
Miller, D.: Abstract syntax for variable binders: an overview. In: Lloyd, J., et al. (eds.) Computational Logic—CL 2000, number 1861 in LNAI, pp. 239–253. Springer (2000)Google Scholar
24. 24.
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51, 125–157 (1991)
25. 25.
Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749–783 (2005)
26. 26.
Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2, 119–141 (1992)
27. 27.
Nadathur, G., Miller, D.: An overview of λProlog. In: Fifth International Logic Programming Conference, Seattle, pp. 810–827. MIT Press (1988)Google Scholar
28. 28.
Nadathur, G., Mitchell, D.J.: System description: Teyjus—a compiler and abstract machine based implementation of λProlog. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, Trento, pp. 287–291. Springer (1999)Google Scholar
29. 29.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer (2002). LNCS Tutorial 2283Google Scholar
30. 30.
Pfenning, F., Schürmann, C.: System description: Twelf—a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, Trento, pp. 202–206. Springer (1999)Google Scholar
31. 31.
Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM Symposium on Principles of Programming Languages (POPL’08), pp. 371–382. ACM (2008)Google Scholar
32. 32.
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)
33. 33.
Plotkin, G.: Call-by-name, call-by-value and the λ-calculus. Theor. Comp. Sci. 1(1), 125–159 (1976)
34. 34.
Plotkin, G.: LCF as a programming language. Theor. Comp. Sci. 5, 223–255 (1977)
35. 35.
Plotkin, G.: A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark (1981)Google Scholar
36. 36.
Poswolsky, A., Schürmann, C.: System description: Delphin—a functional programming language for deductive systems. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), vol. 228, pp. 113–120 (2008)Google Scholar
37. 37.
Reynolds, J.: Definitional interpreters for higher order programming languages. In: ACM Conference Proceedings, pp. 717–740. ACM (1972)Google Scholar
38. 38.
Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Inf. Comput. 111(1), 120–153 (1994)
39. 39.
Schürmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University (2000). CMU-CS-00-146Google Scholar
40. 40.
Smorynski, C.: Modal logic and self-reference. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, vol. 11, 2nd edn., pp. 1–54. Kluwer Academic (2004)Google Scholar
41. 41.
Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (2004)Google Scholar
42. 42.
Tiu, A.: A logic for reasoning about generic judgments. In: Momigliano, A., Pientka, B. (eds.) Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’06) (2006)Google Scholar
43. 43.
Tiu, A., Momigliano, A.: Induction and Co-Induction in Sequent Calculus. Available from http://arxiv.org/abs/0812.4727 (2009)
44. 44.
Urban, C.: Nominal reasoning techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)

## Authors and Affiliations

1. 1.INRIA Saclay—Île-de-France & LIX/École PolytechniquePalaiseauFrance
2. 2.Department of Computer Science and EngineeringUniversity of MinnesotaMinneapolisUSA