Type classes for mathematics in type theory

Article, Preprint OPEN
Spitters, B.A.W. ; Weegen, E.E. van der (2011)
  • Publisher: CAMBRIDGE UNIV PRESS
  • Journal: Mathematical Structures in Computer Science (issn: 0960-1295, eissn: 1469-8072)
  • Related identifiers: doi: 10.1017/S0960129511000119
  • Subject: Computer Science - Logic in Computer Science

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to m... View more
  • References (38)
    38 references, page 1 of 4

    1. M. Armand, B. Gregoire, A. Spiwack, and L. Thery. Extending Coq with imperative features and its application to SAT veri cation. In Interactive Theorem Proving, ITP 2010, Edinburgh, Scotland, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010.

    2. A. Asperti, W. Ricciotti, C.S. Coen, and E. Tassi. Hints in uni cation. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, page 98. Springer, 2009.

    3. A. Asperti, C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. User interaction with the Matita proof assistant. Journal of Automated Reasoning, 39(2):109{139, 2007.

    4. G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Programming, 13(2):261{293, 2003. Special issue on \Logical frameworks and metalanguages".

    5. Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004.

    6. Errett A. Bishop. Foundations of constructive analysis. McGraw-Hill Publishing Company, Ltd., 1967.

    7. S. Boldo, J.C. Filli^atre, and G. Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In Proceedings of the 16th Symposium, 8th International Conference. Held as Part of CICM'09 on Intelligent Computer Mathematics, page 74. Springer, 2009.

    8. T. H. Brus, C. J. D. van Eekelen, M. O. van Leer, and M. J. Plasmeijer. Clean: A language for functional graph rewriting. In Proc. of a conference on Functional programming languages and computer architecture, pages 364{384, London, UK, 1987. Springer-Verlag.

    9. V. Capretta. Universal algebra in type theory. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, TPHOLs 1999, volume 1690 of LNCS, pages 131{148. Springer, 1999.

    10. J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, University of Oxford, 1978.

  • Metrics
    No metrics available
Share - Bookmark