Skip to main content
SpringerLink
Log in

Coq Modulo Theory

  • Conference paper
Book cover Computer Science Logic (CSL 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6247))

Included in the following conference series:

Abstract

Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs.

CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures.

We present here CoqMT, and outline its meta-theoretical study. We also give a brief description of our CoqMT implementation.

This work was partly supported by the ANR ANR-08-BLAN-0326-01.

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. Coq-Development-Team: The Coq Proof Assistant Reference Manual - Version 8.2. INRIA, INRIA Rocquencourt, France (2009), http://coq.inria.fr/

  2. Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76(2-3), 95–120 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  3. Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)

    Google Scholar 

  4. Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, University of Paris VII (1994)

    Google Scholar 

  5. Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  6. Blanqui, F.: Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005); Journal version of LICS 2001

    Google Scholar 

  7. Blanqui, F.: Inductive types in the calculus of algebraic constructions. Fundamenta Informaticae 65(1-2), 61–86 (2005); Journal version of TLCA 2003

    MATH  MathSciNet  Google Scholar 

  8. Stehr, M.: The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II). Fundamenta Informaticae 68 (2005)

    Google Scholar 

  9. Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278–293. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: LICS, pp. 208–212. IEEE Computer Society, Los Alamitos (1994)

    Google Scholar 

  11. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  12. Blanqui, F., Jouannaud, J., Strub, P.: Building decision procedures in the calculus of inductive constructions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 328–342. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Strub, P.Y.: Type Theory and Decision Procedures. PhD thesis, École Polytechnique (2008)

    Google Scholar 

  14. Barendregt, H.P.: Lambda calculi with types, pp. 117–309 (1992)

    Google Scholar 

  15. Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 243–320 (1990)

    Google Scholar 

  16. Courtieu, P.: Normalized types. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 554–569. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Petcher, A., Stump, A.: Deciding joinability modulo ground equations in operational type theory. In: Proof Search in Type Theories, PSTT (2009)

    Google Scholar 

  18. Shostak, R.E.: An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery 26(2), 351–360 (1979)

    MATH  MathSciNet  Google Scholar 

  19. Barbanera, F., Fernández, M., Geuvers, H.: Modularity of strong normalization and confluence in the algebraic-lambda-cube. In: LICS, pp. 406–415. IEEE Computer Society, Los Alamitos (1994)

    Google Scholar 

  20. Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)

    MATH  Google Scholar 

  21. Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, Tsinghua University, Offices 3-604, FIT Building, Haidian District, Beijing, 100084, China

    Pierre-Yves Strub

Authors
  1. Pierre-Yves Strub
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Laboratory, University of Cambridge, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  2. Formal Methods in Systems Engineering, Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Helmut Veith

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Strub, PY. (2010). Coq Modulo Theory. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_40

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15205-4_40

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15204-7

  • Online ISBN: 978-3-642-15205-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation