Experience Implementing a Performant Category-Theory Library in Coq: Complete List of References

[1] Wikipedia. Adjoint functors: Formal definitions: Universal morphisms, December 2013. [ bib | http ]
[2] Li Nuo. Second-year annual report, July 2013. [ bib | .pdf ]
[3] Yves Bertot. Private inductive types: Proposing a language extension, April 2013. [ bib | .pdf ]
For the Coq system, we propose to add the possibility to declare an inductive type as private to the module where it is defined. The effect is to preserve the possibility to compute with a restricted set of functions, but to disallow uses of the more powerful pattern-matching constructs. Such a private type has fruitful applications in homotopy type theory.
[4] Benedikt Ahrens, Chris Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. ArXiv e-prints, March 2013. [ bib | arXiv | http ]
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of "category" for which equality and equivalence of categories agree. Such categories satisfy a version of the Univalence Axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them "saturated" or "univalent" categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
Keywords: Mathematics - Category Theory, Mathematics - Logic, 18A15
[5] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Lulu Marketplace, 2013. [ bib | http ]
[6] nCatLab. adjoint functor: in terms of universal arrows / universal factorization through unit and counit, November 2012. [ bib | http ]
[7] nCatLab. subobject classifier, September 2012. [ bib | http ]
[8] Olov Wilander. Constructing a small category of setoids. Mathematical Structures in Computer Science, 22(1):103--121, 2012. [ bib | .pdf ]
[9] Ulf Norell. Agda performance improvements, August 2011. [ bib | .html ]
[10] Michael Shulman. An interval type implies function extensionality, April 2011. [ bib | http ]
[11] Arnaud Spiwack. Verified computing in homological algebra. Phd thesis, École Polytechnique, 2011. [ bib | .pdf ]
[12] Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. In ACM SIGPLAN Notices, volume 46, pages 163--175. ACM, 2011. [ bib | .pdf ]
[13] Alexander Katovsky. Category theory. Archive of Formal Proofs, June 2010. http://afp.sf.net/entries/Category2.shtml, Formal proof development. [ bib | .pdf ]
This article presents a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases.
[14] Bas Spitters and Eelis van der Weegen. Developing the algebraic hierarchy with type classes in coq. In Interactive Theorem Proving, pages 490--493. Springer, 2010. [ bib | .pdf ]
[15] Milad Niqui. Coalgebras, bisimulation and lambda-coiteration, January 2010. [ bib | http ]
[16] Steve Awodey. Category theory. Oxford University Press, second edition edition, 2010. [ bib ]
[17] Benedikt Ahrens. Categorical semantics of programming languages (in Coq), 2010. [ bib | .pdf ]
[18] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 327--342. Springer Berlin Heidelberg, 2009. [ bib | DOI | .pdf ]
This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm, and a matrix decomposition problem.
Keywords: Formalization of Algebra; Coercive subtyping; Type inference; Coq; SSReflect
[19] Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. In FoSSaCS, pages 365--379, 2008. [ bib | .pdf ]
[20] Tom Leinster. Higher Operads, Higher Categories. Cambridge Univ. Press, 2007. [ bib | arXiv | http ]
Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. This is the first book on the subject and lays its foundations. Many examples are given throughout. There is also an introductory chapter motivating the subject for topologists.
[21] Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Proceedings of the 2007 workshop on Programming languages meets program verification, pages 57--68. ACM, 2007. [ bib | .pdf ]
[22] Dexter Kozen, Christoph Kreitz, and Eva Richter. Automating proofs in category theory. In Automated Reasoning, pages 392--407. Springer, 2006. [ bib | .pdf ]
[23] Thorsten Altenkirch and Conor McBride. Towards observational type theory. Manuscript, available online, 2006. [ bib | .pdf ]
[24] Olov Wilander. An E-bicategory of E-categories exemplifying a type-theoretic approach to bicategories. Technical report, Technical report, University of Uppsala, 2005. [ bib | http ]
[25] Greg O'Keefe. Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, 91:212--228, 2004. [ bib | .pdf ]
[26] Tjark Weber. Program transformations in Nuprl. Master's thesis, University of Wyoming, Laramie, WY, August 2002. [ bib | .html | .pdf ]
[27] Mario Jose Cáccamo and Glynn Winskel. A higher-order calculus for categories. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, volume 2152 of Lecture Notes in Computer Science, pages 136--153. Springer Berlin Heidelberg, June 2001. [ bib | DOI | .pdf ]
A calculus for a fragment of category theory is presented. The types in the language denote categories and the expressions functors. The judgements of the calculus systematise categorical arguments such as: an expression is functorial in its free variables; two expressions are naturally isomorphic in their free variables. There are special binders for limits and more general ends. The rules for limits and ends support an algebraic manipulation of universal constructions as opposed to a more traditional diagrammatic approach. Duality within the calculus and applications in proving continuity are discussed with examples. The calculus gives a basis for mechanising a theory of categories in a generic theorem prover like Isabelle.
[28] Alexandre Miquel. The implicit calculus of constructions. In Typed Lambda Calculi and Applications, volume 2044, page 344. Springer, 2001. [ bib | .pdf ]
[29] Gérard Huet and Amokrane Saïbi. Constructive category theory. In Proof, language, and interaction, pages 239--275. MIT Press, 2000. [ bib | DOI | http ]
[30] Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice, 1995), 36:83--111, August 1998. [ bib | .pdf ]
[31] Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer verlag, 1998. [ bib | http ]
[32] Alexandra Carvalho and Paulo Mateus. Category theory in Coq. Technical report, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1998. [ bib | DOI | .ps | .pdf ]
Herein we formalize a segment of category theory using the implementation of Calculus of Inductive Construction in Coq. Adopting the axiomatization proposed by Huet and Saibi we start by presenting basic concepts, examples and results of category theory in Coq. Next we define adjunction and cocartesian lifting and establish some results using the Coq proof assistant. Finally we remark that the axiomatization proposed by Huet and Saibi is not good when dealing with the equality for objects. 1...
Keywords: category-theory, formalization
[33] John Harrison. Formalized mathematics. TUCS technical report. Turku Centre for Computer Science, 1996. [ bib | DOI | http ]
[34] Sten Agerholm. Experiments in formalizing basic category theory in higher order logic and set theory. Draft manuscript, December 1995. [ bib | DOI | http ]
[35] Takahisa Mohri. On formalization of category theory. Master's thesis, University of Tokyo, 1995. [ bib | .ps | .pdf ]
[36] Peter Aczel. Galois: a theory development project. A report on work in progress for the Turin meeting on the Representation of Logical Frameworks, 1993. [ bib | .ps.gz | .pdf ]
[37] Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89(1):107 -- 136, 1991. [ bib | DOI | http ]
Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of “universes”, each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure properties of type theories) and some practical (to achieve some of the advantages of a type of all types without sacrificing consistency.) The Generalized Calculus of Constructions (CCω) is a formal theory of types that includes such a hierarchy of universes. Although essential to the formalization of constructive mathematics, universes are tedious to use in practice, for one is required to make specific choices of universe levels and to ensure that all choices are consistent. In this paper we study several problems associated with type checking in the presence of universes in the context of CCω. First, we consider the basic type checking and well-typedness problems for this calculus. Second, we consider a formulation of Russell and Whitehead's “typical ambiguity” convention whereby universe levels may be elided, provided that some consistent assignment of levels leads to a correct derivation. Third, we consider the introduction of definitions to both the basic calculus and the calculus with typical ambiguity. This extension leads to a notion of “universe polymorphism” analogous to the type polymorphism of ML. Although our study is conducted for CCω, we expect that our methods will apply to other variants of the Calculus of Constructions and to type theories such as Constable's V3.
[38] James A Altucher and Prakash Panangaden. A mechanically assisted constructive proof in category theory. In 10th International Conference on Automated Deduction, pages 500--513. Springer, 1990. [ bib | http ]
[39] B. Pierce. A taste of category theory for computer scientists. Technical report, Carnegie Mellon University, 1988. [ bib | http ]
[40] Roy Dyckhoff. Category theory as an extension of martin-löf type theory. Technical report, University of St. Andrews, 1985. [ bib | .pdf ]
[41] Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis, 1984. [ bib | .pdf ]
[42] Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill series in higher mathematics. McGraw-Hill, 1967. [ bib | http ]
[43] Formalizations of category theory in proof assistants. [ bib | http ]
[44] Jason Gross. HoTT/HoTT categories. [ bib | http ]
[45] The Coq proof assistant. [ bib | http ]
[46] Matthieu Sozeau, Hugo Herbelin, Pierre Letouzey, Jean-Christophe Filliâtre, Matthieu Sozeau, anonymous, Pierre-Marie Pédrot, Bruno Barras, Jean-Marc Notin, Pierre Boutillier, Enrico Tassi, Stéphane Glondu, Arnaud Spiwack, Claudio Sacerdoti Coen, Christine Paulin, Olivier Desmettre, Yves Bertot, Julien Forest, David Delahaye, Pierre Corbineau, Julien Narboux, Matthias Puech, Benjamin Monate, Elie Soubiran, Pierre Courtieu, Vincent Gross, Judicaël Courant, Lionel Elie Mamane, Clément Renard, Evgeny Makarov, Claude Marché, Guillaume Melquiond, Micaela Mayero, Yann Régis-Gianas, Benjamin Grégoire, Vincent Siles, Frédéric Besson, Laurent Théry, Florent Kirchner, Maxime Dénès, Xavier Clerc, Loïc Pottier, Russel O'Connor, Assia Mahboubi, Benjamin Werner, xclerc, Huang Guan-Shieng, Jason Gross, Tom Hutchinson, Cezary Kaliszyk, Pierre, Daniel De Rauglaudre, Alexandre Miquel, Damien Doligez, Gregory Malecha, Stephane Glondu, and Andrej Bauer. HoTT/coq. [ bib | http ]
[47] Matthieu Sozeau. Cat. [ bib | http ]
[48] Matthieu Sozeau. mattam82/coq polyproj. [ bib | http ]
[49] Carlos Simpson. CatsInZFC. [ bib | http ]
[50] Amokrane Saïbi. Constructive category theory. [ bib | http ]
[51] Nicolas Pouillard. crypto-agda/crypto-agda. [ bib | http ]
[52] Loïc Pottier. Algebra. [ bib | http ]
[53] Daniel Peebles, James Deikun, Andrea Vezzosi, and James Cook. copumpkin/categories. [ bib | http ]
[54] Adam Megacz. Category theory library for Coq. [ bib | http ]
[55] Robbert Krebbers, Bas Spitters, and Eelis van der Weegen. Math classes. [ bib | http ]
[56] Vladimir Komendantsky, Alexander Konovalov, and Steve Linton. Connecting Coq theorem prover to GAP. [ bib | .pdf ]
[57] Hiromi Ishii. konn/category-agda. [ bib | http ]
[58] James Chapman. jmchapman/restriction-categories. [ bib | http ]
[59] Paolo Capriotti. pcapriotti/agda-categories. [ bib | http ]
[60] Benedikt Ahrens, Chris Kapulkin, and Michael Shulman. benediktahrens/rezk_completion. [ bib | http ]
[61] Benedikt Ahrens. benediktahrens/Foundations typesystems. [ bib | http ]
[62] Benedikt Ahrens. Coinductives. [ bib | http ]

This file was generated by bibtex2html 1.99.