Document Open Access Logo

A Two-Level Logic Approach to Reasoning About Typed Specification Languages

Authors Mary Southern, Kaustuv Chaudhuri

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.557.pdf
  • Filesize: 0.53 MB
  • 13 pages

Document Identifiers

Author Details

Mary Southern
Kaustuv Chaudhuri

Cite As Get BibTex

Mary Southern and Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning About Typed Specification Languages. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 557-569, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.557

Abstract

The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.

Subject Classification

Keywords
  • Abella theorem prover
  • two-level logic
  • typed specification languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Olivier Savary Bélanger and Kaustuv Chaudhuri. Automatically deriving schematic theorems for dynamic contexts. In LFMTP'14, pages 9:1-9:8. ACM, 2014. Google Scholar
  2. Andrew Cave and Brigitte Pientka. Programming with binders and indexed data-types. In POPL, pages 413-424. ACM, 2012. Google Scholar
  3. Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In CADE, volume 449 of LNAI, pages 221-235. Springer, 1990. Google Scholar
  4. Andrew Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, 2009. Google Scholar
  5. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. Google Scholar
  6. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241-273, 2012. Google Scholar
  7. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  8. Dale Miller and Gopalan Nadathur. A computational logic approach to syntax and semantics. 10th Symp. of the Mathematical Foundations of Computer Science, May 1985. Google Scholar
  9. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. Google Scholar
  10. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. Google Scholar
  11. Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus - A compiler and abstract machine based implementation of λProlog. In CADE, number 1632 in Lecture Notes in Artificial Intelligence, pages 287-291. Springer, 1999. Google Scholar
  12. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual model type theory. ACM Trans. on Computational Logic, 9(3):1-49, 2008. Google Scholar
  13. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In PLDI, pages 199-208. ACM Press, June 1988. Google Scholar
  14. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pages 202-206, Trento, 1999. Springer. Google Scholar
  15. Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In IJCAR, pages 15-21. Springer LNCS 6173, 2010. Google Scholar
  16. Adam Poswolsky and Carsten Schürmann. System description: Delphin - A functional programming language for deductive systems. In LFMTP, volume 228, pages 113-120, 2008. Google Scholar
  17. Zachary Snow, David Baelde, and Gopalan Nadathur. A meta-programming approach to realizing dependently typed logic programming. In PPDP, pages 187-198, 2010. Google Scholar
  18. Mary Southern and Gopalan Nadathur. A λProlog based animation of Twelf specifications, July 2014. Available at URL: http://arxiv.org/abs/1407.1545.
  19. Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopalan Nadathur. Reasoning about higher-order relational specifications. In PPDP, pages 157-168, Madrid, Spain, September 2013. Google Scholar
  20. The Abella web-site. http://abella-prover.org/, 2013.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact