Universal Algebra in Type Theory

  • Venanzio Capretta
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1690)


We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. We use setoids, i.e. types endowed with an arbitrary equivalence relation, as carriers for algebras. In this way it is possible to define the quotient of an algebra by a congruence. Standard constructions over algebras are defined and their basic properties are proved formally. To overcome the problem of defining term algebras in a uniform way, we use types of trees that generalize wellorderings. Our implementation gives tools to define new algebraic structures, to manipulate them and to prove their properties.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Peter Aczel. Notes towards a formalisation of constructive galois theory. draft report, 1994.Google Scholar
  2. [2]
    H. P. Barendregt. Lambda Calculi with Types. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 2. Oxford University Press, 1992.Google Scholar
  3. [3]
    Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, Henri Laulhère, César Muñoz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick Loiseleur, Christine Paulin-Mohring, Amokrane Saïbi, and Benjanin Werner. The Coq Proof Assistant Reference Manual. Version 6.2.Google Scholar
  4. [4]
    G. Barthe, M. Ruys, and H. P. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs (TYPES’95), volume LNCS 1158, pages 16–35. Springer, 1995.CrossRefGoogle Scholar
  5. [5]
    Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software. Third International Symposium, TACS’97, volume LNCS 1281, pages 515–529. Springer, 1997.CrossRefGoogle Scholar
  6. [6]
    R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.Google Scholar
  7. [7]
    Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-Löf, editor, Proceedings of Colog’ 88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.Google Scholar
  8. [8]
    Thierry Coquand and Henrik Persson. Integrated Development of Algebra in Type Theory. Presented at the Calculemus and Types’ 98 workshop, 1998.Google Scholar
  9. [9]
    Eduardo Giménez. A Tutorial on Recursive Types in Coq. Technical report, Unité de recherche INRIA Rocquencourt, 1998.Google Scholar
  10. [10]
    Martin Hofmann. Elimination of extensionality in Martin-Löf type theory. In Barendregt and Nipkow, editors, Types for Proofs and Programs. International Workshop TYPES’ 93, pages 166–90. Springer-Verlag, 1993.Google Scholar
  11. [11]
    Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 208–212. IEEE Computer Society Press, 1994.Google Scholar
  12. [12]
    Douglas J. Howe. Computational metatheory in Nuprl. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, volume LNCS 310, pages 238–257. Springer-Verlag, 1988.CrossRefGoogle Scholar
  13. [13]
    Gérard Huet and Amokrane Saïbi. Constructive category theory. In In honor of Robin Milner. Cambridge University Press, 1997.Google Scholar
  14. [14]
    Paul Jackson. Exploring abstract algebra in constructive type theory. In Automated Deduction — CADE-12, volume Lectures Notes in Artificial Intelligence 814, pages 591–604. Springer-Verlag, 1994.Google Scholar
  15. [15]
    Zhaohui Luo. Computation and Reasoning, A Type Theory for Computer Science, volume 11 of International Series of Monographs on Computer Science. Oxford University Press, 1994.Google Scholar
  16. [16]
    Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153–175. North-Holland, 1982.Google Scholar
  17. [17]
    Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.Google Scholar
  18. [18]
    K. Meinke and J. V. Tucker. Universal Algebra. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 1. Oxford University Press, 1992.Google Scholar
  19. [19]
    Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory. Clarendon Press, 1990.Google Scholar
  20. [20]
    Kent Petersson and Dan Synek. A Set Constructor for Inductive Sets in Martin-Löf’s Type Theory. In Proceedings of the 1989 Conference on Category Theory and Computer Science, Manchester, U.K., volume 389 of Lecture Notes in Computer Science. Springer-Verlag, 1989.Google Scholar
  21. [21]
    Amokrane Saïbi. Typing algorithm in type theory with inheritance. In POPL’97: The 12th ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages, pages 292–301. Association for Computing Machinery, 1997.Google Scholar
  22. [22]
    Milena Stefanova. Properties of Typing Systems. PhD thesis, Computer Science Institute, University of Nijmegen, 1999.Google Scholar
  23. [23]
    Laurent Théry. Proving and Computing: a certified version of the Buchberger’s algorithm. Technical report, INRIA, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Venanzio Capretta
    • 1
  1. 1.Computer Science InstituteUniversity of NijmegenUSA

Personalised recommendations