Skip to main content
SpringerLink
Log in

Two-Level Meta-reasoning in Coq

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2410))

Included in the following conference series:

Abstract

The use of higher-order abstract syntax is central to the direct, concise, and modular specification of languages and deductive systems in a logical framework. Developing a framework in which it is also possible to reason about such deductive systems is particularly challenging. One difficulty is that the use of higher-order abstract syntax complicates reasoning by induction because it leads to definitions for which there are no monotone inductive operators. In this paper, we present a methodology which allows Coq to be used as a framework for such meta-reasoning. This methodology is directly inspired by the two-level approach to reasoning used in the FOλΔℕ (pronounced fold-n) logic. In our setting, the Calculus of Inductive Constructions (CIC) implemented by Coq represents the highest level, or meta-logic, and a separate specification logic is encoded as an inductive definition in Coq. Then, in our method as in FOλΔℕ, the deductive systems that we want to reason about are the object logics which are encoded in the specification logic. We first give an approach to reasoning in Coq which very closely mimics reasoning in FOλΔℕillustrating a close correspondence between the two frameworks. We then generalize the approach to take advantage of other constructs in Coq such as the use of direct structural induction provided by inductive types.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A.W. Appel and A.P. Felty. Lightweight lemmas in λProlog. In International Conference on Logic Programming, Nov. 1999.

    Google Scholar 

  2. A.W. Appel and A.P. Felty. A semantic model of types and machine instructions for proof-carrying code. In The 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2000.

    Google Scholar 

  3. P. Borras, D. Clément, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. Centaur: The system. In Proceedings of SIGSOFT’88: Third Annual Symposium on Software Development Environments (SDE3), Boston, 1988.

    Google Scholar 

  4. J. Despeyroux. A higher-order specification of the π-calculus. In First IFIP International Conference on Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science, 2000.

    Google Scholar 

  5. J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications. Springer-Verlag Lecture Notes in Computer Science, Apr. 1995.

    Google Scholar 

  6. J. Despeyroux and A. Hirschowitz. Higher-order syntax and induction in coq. In Fifth International Conference on Logic Programming and Automated Reasoning. Springer-Verlag Lecture Notes in Computer Science, 1994.

    Google Scholar 

  7. J. Despeyroux, F. Pfenning, and C. Schürmann. Primitive recursion for higher-order abstract syntax. In Third International Conference on Typed Lambda Calculi and Applications. Springer-Verlag Lecture Notes in Computer Science, 1997.

    Google Scholar 

  8. L.-H. Eriksson. A finitary version of the calculus of partial inductive definitions. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the January 1991 Workshop on Extensions to Logic Programming. Springer-Verlag Lecture Notes in Artificial Intelligence, 1992.

    Google Scholar 

  9. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1), Jan. 1993.

    Google Scholar 

  10. M. Hofmann. Semantical analysis of higher-order abstract syntax. In Fourteenth Annual Symposium on Logic in Computer Science, 1999.

    Google Scholar 

  11. F. Honsell, M. Miculan, and I. Scagnetto. π-calculus in (co)inductive type theories. Theoretical Computer Science, 253(2), 2001.

    Google Scholar 

  12. R. McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, December 1997.

    Google Scholar 

  13. R. McDowell and D. Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1), Jan. 2002.

    Google Scholar 

  14. M. Miculan. Developing (meta)theory of λ-calculus in the theory of contexts. Electronic Notes on Theoretical Computer Science, 58, 2001.

    Google Scholar 

  15. M. Miculan. On the formalization of the modal μ-calculus in the calculus of inductive constructions. Information and Computation, 164(1), 2001.

    Google Scholar 

  16. G. Nadathur and D. Miller. An overview of λProlog. In K. Bowen and R. Kowalski, editors, Fifth International Conference and Symposium on Logic Programming. MIT Press, 1988.

    Google Scholar 

  17. G. Necula. Proof-carrying code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, Jan. 1997.

    Google Scholar 

  18. F. Pfenning and E. Rohwedder. Implementing the meta-theory of deductive systems. In Eleventh International Conference on Automated Deduction, volume 607. Lecture Notes in Computer Science, 1992.

    Google Scholar 

  19. F. Pfenning and C. Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In Sixteenth International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1999.

    Google Scholar 

  20. C. Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University, 2000.

    Google Scholar 

  21. The Coq Development Team. The Coq Proof Assistant reference manual: Version 7.2. Technical report, INRIA, 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Engineering, University of Ottawa, Ottawa, Ontario, K1N 6N5, Canada

    Amy P. Felty

Authors
  1. Amy P. Felty
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, Hampton, VA, 23681, USA

    Victor A. Carreño

  2. ICASE-Langley Research Center, MS 132C, Hampton, VA, 23681, USA

    César A. Muñoz

  3. Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd.W., Montréal, Québec, H3G 1M8, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Felty, A.P. (2002). Two-Level Meta-reasoning in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45685-6_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44039-0

  • Online ISBN: 978-3-540-45685-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation