Skip to main content
SpringerLink
Log in

A Two-Level Logic Approach to Reasoning About Computations

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  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)

  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)

  3. Baelde, D.: A Linear Approach to the Proof-Theory of Least and Greatest Fixed Points. PhD thesis, Ecole Polytechnique (2008)

  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)

  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)

  6. Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  7. Coquand, T., Paulin, C.: Inductively defined types. In: Conference on Computer Logic. LNCS, vol. 417, pp. 50–66. Springer (1988)

  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)

  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)

  10. Felty, A., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. (2010). doi:10.1007/s10817-010-9194-x

    Google Scholar 

  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. Gacek, A.: The Abella System and Homepage. http://abella.cs.umn.edu/ (2009)

  13. Gacek, A.: A Framework for Specifying, Prototyping, and Reasoning About Computational Systems. PhD thesis, University of Minnesota (2009)

  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. Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48–73 (2011)

    Article  MathSciNet  Google Scholar 

  16. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  17. Kahn, G.: Natural semantics. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 247, pp. 22–39. Springer (1987)

  18. Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(5), 308–320 (1964)

    MATH  Google Scholar 

  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)

  20. McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theor. Comp. Sci. 232, 91–119 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  21. McDowell, R., Miller, D. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3(1), 80–136 (2002)

    Article  MathSciNet  Google Scholar 

  22. Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358 (1992)

    Article  MATH  Google Scholar 

  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)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  25. Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749–783 (2005)

    Article  MathSciNet  Google Scholar 

  26. Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2, 119–141 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  27. Nadathur, G., Miller, D.: An overview of λProlog. In: Fifth International Logic Programming Conference, Seattle, pp. 810–827. MIT Press (1988)

  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)

  29. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer (2002). LNCS Tutorial 2283

  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)

  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)

  32. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  33. Plotkin, G.: Call-by-name, call-by-value and the λ-calculus. Theor. Comp. Sci. 1(1), 125–159 (1976)

    MathSciNet  Google Scholar 

  34. Plotkin, G.: LCF as a programming language. Theor. Comp. Sci. 5, 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  35. Plotkin, G.: A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark (1981)

  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)

  37. Reynolds, J.: Definitional interpreters for higher order programming languages. In: ACM Conference Proceedings, pp. 717–740. ACM (1972)

  38. Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Inf. Comput. 111(1), 120–153 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  39. Schürmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University (2000). CMU-CS-00-146

  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)

  41. Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (2004)

  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)

  43. Tiu, A., Momigliano, A.: Induction and Co-Induction in Sequent Calculus. Available from http://arxiv.org/abs/0812.4727 (2009)

  44. Urban, C.: Nominal reasoning techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Saclay—Île-de-France & LIX/École Polytechnique, Palaiseau, France

    Andrew Gacek & Dale Miller

  2. Department of Computer Science and Engineering, University of Minnesota, 4-192 EE/CS Building, 200 Union Street SE, Minneapolis, MN, 55455, USA

    Gopalan Nadathur

Authors
  1. Andrew Gacek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dale Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gopalan Nadathur
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dale Miller.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gacek, A., Miller, D. & Nadathur, G. A Two-Level Logic Approach to Reasoning About Computations. J Autom Reasoning 49, 241–273 (2012). https://doi.org/10.1007/s10817-011-9218-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-011-9218-1

Keywords

Search

Navigation