Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Peter Aczel. Notes towards a formalisation of constructive galois theory. draft report, 1994.
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.
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.
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.
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.
R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
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.
Thierry Coquand and Henrik Persson. Integrated Development of Algebra in Type Theory. Presented at the Calculemus and Types’ 98 workshop, 1998.
Eduardo Giménez. A Tutorial on Recursive Types in Coq. Technical report, Unité de recherche INRIA Rocquencourt, 1998.
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.
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.
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.
Gérard Huet and Amokrane Saïbi. Constructive category theory. In In honor of Robin Milner. Cambridge University Press, 1997.
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.
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.
Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153–175. North-Holland, 1982.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
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.
Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory. Clarendon Press, 1990.
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.
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.
Milena Stefanova. Properties of Typing Systems. PhD thesis, Computer Science Institute, University of Nijmegen, 1999.
Laurent Théry. Proving and Computing: a certified version of the Buchberger’s algorithm. Technical report, INRIA, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Capretta, V. (1999). Universal Algebra in Type Theory. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_10
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive