Edit Profile (opens in new tab) Coquand, Thierry Co-Author Distance Author ID: coquand.thierry Published as: Coquand, Thierry; Coquand, T. Homepage: http://www.cse.chalmers.se/~coquand/ External Links: MGP · Wikidata · ResearchGate · dblp · GND · IdRef · theses.fr Videos: carmin.tv Documents Indexed: 184 Publications since 1984, including 13 Additional arXiv Preprints 7 Contributions as Editor · 1 Further Contribution Reviewing Activity: 34 Reviews Co-Authors: 85 Co-Authors with 144 Joint Publications 1,266 Co-Co-Authors all top 5 Co-Authors 48 single-authored 25 Lombardi, Henri 14 Bezem, Marc 8 Abel, Andreas M. 8 Huber, Simon 8 Neuwirth, Stefan 8 Spitters, Bas 7 Dybjer, Peter 7 Quitté, Claude 6 Schuster, Peter Michael 5 Breazu-Tannen, Val 5 Gunter, Carl A. 5 Mannaa, Bassel 5 Mörtberg, Anders 5 Palmgren, Erik 5 Sambin, Giovanni 5 Smith, Jan M. 4 Altenkirch, Thorsten 4 Hötzel Escardó, Martín 4 Huet, Gerard P. 4 Sattler, Christian 4 Siles, Vincent 4 Takeyama, Makoto 3 Barthe, Gilles 3 Berardi, Stefano 3 Cohen, Cyril 3 Kraus, Nicolai 3 Nordström, Bengt 3 Persson, Henrik 3 Ščedrov, Andrej 3 Spiwack, Arnaud 2 Angiuli, Carlo 2 Awodey, Steve 2 Barras, Bruno 2 Bauer, Andrej 2 Brunerie, Guillaume 2 Cederquist, Jan 2 Cherubini, Felix 2 Dawar, Anuj 2 Harper, Robert 2 Herbelin, Hugo 2 Hofmann, Martin 2 Hou (Favonia), Kuen-Bang 2 Hutzler, Matthias 2 Jaber, Guilhem 2 Maietti, Maria Emilia 2 Negri, Sara 2 Pagano, Miguel 2 Pollack, Randy 2 Quadrat, Alban 2 Riehl, Emily 2 Ruch, Fabian 2 Tête, Claire 2 Winskel, Glynn 2 Zhang, Guo-Qiang 1 Aczel, Peter 1 Ahrens, Benedikt 1 Alonso García, María Emilia 1 Avigad, Jeremy 1 Banaschewski, Bernhard 1 Barakat, Mohamed 1 Bernardy, Jean-Philippe 1 Bertot, Yves 1 Bordg, Anthony 1 Bove, Ana 1 Buchholtz, Ulrik 1 Cavallo, Evan 1 Constable, Robert Lee 1 Coquand, Catarina 1 Curien, Pierre-Louis 1 Danielsson, Nils Anders 1 Ducos, Lionel 1 Ehrhard, Thomas 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Hayashi, Susumu 1 Heras, Jónathan 1 Hofstra, Pieter J. W. 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kinoshita, Yoshiki 1 Kock, Joachim 1 Li, Nuo 1 Licata, Dan 1 Licata, Daniel R. 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Moulin, Guilhem 1 Nahas, Michael 1 Niwiński, Damian 1 Norell, Ulf 1 Parmann, Erik 1 Paulin, Christine 1 Pelayo, Alvaro ...and 24 more Co-Authors all top 5 Serials 8 Theoretical Computer Science 8 Annals of Pure and Applied Logic 7 Mathematical Structures in Computer Science 7 Logical Methods in Computer Science 6 Journal of Logic and Analysis 5 The Journal of Symbolic Logic 5 Fundamenta Informaticae 4 Journal of Algebra 4 Journal of Pure and Applied Algebra 4 Information and Computation 4 Archive for Mathematical Logic 3 Indagationes Mathematicae. New Series 3 Mathematical Logic Quarterly (MLQ) 3 Journal of Functional Programming 2 Mathematical Proceedings of the Cambridge Philosophical Society 2 Manuscripta Mathematica 2 Journal of Symbolic Computation 2 Comptes Rendus de l’Académie des Sciences. Série I 2 Oberwolfach Reports 1 American Mathematical Monthly 1 Communications in Algebra 1 Rocky Mountain Journal of Mathematics 1 Archiv der Mathematik 1 BIT 1 Gazette des Mathématiciens 1 Science of Computer Programming 1 History and Philosophy of Logic 1 Journal of Automated Reasoning 1 Bulletin of the European Association for Theoretical Computer Science (EATCS) 1 Bulletin of the American Mathematical Society. New Series 1 Annals of Mathematics and Artificial Intelligence 1 Theory of Computing Systems 1 Positivity 1 Bulletin of the European Association for Theoretical Computer Science EATCS 1 La Gaceta de la Real Sociedad Matemática Española 1 Journal of Universal Computer Science 1 Comptes Rendus. Mathématique. Académie des Sciences, Paris 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 ACM Transactions on Computational Logic 1 Journal of Algebra and its Applications 1 Lecture Notes in Computer Science 1 Journal of Formalized Reasoning all top 5 Fields 156 Mathematical logic and foundations (03-XX) 65 Computer science (68-XX) 30 Commutative algebra (13-XX) 25 Order, lattices, ordered algebraic structures (06-XX) 19 Category theory; homological algebra (18-XX) 12 Algebraic geometry (14-XX) 12 General topology (54-XX) 12 Algebraic topology (55-XX) 9 General and overarching topics; collections (00-XX) 7 History and biography (01-XX) 6 Functional analysis (46-XX) 5 Combinatorics (05-XX) 5 Measure and integration (28-XX) 2 Field theory and polynomials (12-XX) 2 Associative rings and algebras (16-XX) 1 General algebraic systems (08-XX) 1 Number theory (11-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 \(K\)-theory (19-XX) 1 Group theory and generalizations (20-XX) 1 Topological groups, Lie groups (22-XX) 1 Functions of a complex variable (30-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Abstract harmonic analysis (43-XX) 1 Numerical analysis (65-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Systems theory; control (93-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 141 Publications have been cited 1,653 times in 1,015 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002 The Univalent Foundations Program 254 2013 The calculus of constructions. Zbl 0654.03045 Coquand, Thierry; Huet, Gérard 214 1988 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036 Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 85 2018 A model of type theory in cubical sets. Zbl 1359.03009 Bezem, Marc; Coquand, Thierry; Huber, Simon 70 2014 Inductively generated formal topologies. Zbl 1070.03041 Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio 67 2003 Inductively defined types. Zbl 0722.03006 Coquand, Thierry; Paulin, Christine 52 1990 Constructions: A higher order proof system for mechanizing mathematics. Zbl 0581.03007 Coquand, Thierry; Huet, Gérard 44 1985 Entailment relations and distributive lattices. Zbl 0948.03056 Cederquist, Jan; Coquand, Thierry 42 2000 Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507 Coquand, Thierry; Lombardi, Henri 41 2003 Inheritance as implicit coercion. Zbl 0799.68129 Breazu-Tannen, Val; Coquand, Thierry; Gunter, Carl A.; Scedrov, Andre 40 1991 A semantics of evidence for classical arithmetic. Zbl 0829.03037 Coquand, Thierry 38 1995 On the computational content of the axiom of choice. Zbl 0914.03059 Berardi, Stefano; Bezem, Marc; Coquand, Thierry 35 1998 An algorithm for testing conversion in type theory. Zbl 0754.03041 Coquand, Thierry 29 1991 A logical approach to abstract algebra. Zbl 1118.03059 Coquand, Thierry; Lombardi, Henri 28 2006 Domain theoretic models of polymorphism. Zbl 0683.03007 Coquand, Thierry; Gunter, Carl; Winskel, Glynn 27 1989 On higher inductive types in cubical type theory. Zbl 1452.03036 Coquand, Thierry; Huber, Simon; Mörtberg, Anders 27 2018 Infinite objects in type theory. Zbl 1527.03008 Coquand, Thierry 25 1994 Generating non-Noetherian modules constructively. Zbl 1059.13006 Coquand, Thierry; Lombardi, Henri; Quitté, Claude 24 2004 dI-domains as a model of polymorphism. Zbl 0644.68041 Coquand, Thierry; Gunter, Carl; Winskel, Glynn 22 1988 Valuations and Dedekind’s Prague theorem. Zbl 0983.11061 Coquand, Thierry; Persson, Henrik 21 2001 Intuitionistic model constructions and normalization proofs. Zbl 0883.03009 Coquand, Thierry; Dybjer, Peter 20 1997 Automating coherent logic. Zbl 1143.03332 Bezem, Marc; Coquand, Thierry 19 2005 Space of valuations. Zbl 1222.03072 Coquand, Thierry 19 2009 About Stone’s notion of spectrum. Zbl 1061.06031 Coquand, Thierry 18 2005 An elementary characterization of Krull dimension. Zbl 1161.54303 Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise 17 2005 Inheritance and explicit coercion. Zbl 0716.68012 Breazu-Tannen, V.; Coquand, T.; Gunter, C. A.; Scedrov, A. 15 1989 Extensional models for polymorphism. Zbl 0713.03005 Breazu-Tannen, Val; Coquand, Thierry 15 1988 A presheaf model of parametric type theory. Zbl 1351.68146 Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem 15 2015 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069 Coquand, Thierry; Hofmann, Martin 15 1999 Constructive topology and combinatorics. Zbl 1434.03143 Coquand, Thierry 14 1992 An algorithm for type-checking dependent types. Zbl 0853.68102 Coquand, Thierry 14 1996 Proof-theoretical analysis of order relations. Zbl 1062.03055 Negri, Sara; von Plato, Jan; Coquand, Thierry 14 2004 Integrals and valuations. Zbl 1245.03098 Coquand, Thierry; Spitters, Bas 14 2009 Categories of embeddings. Zbl 0688.18004 Coquand, Thierry 13 1989 Sequents, frames, and completeness. Zbl 0973.03080 Coquand, Thierry; Zhang, Guo-Qiang 12 2000 Heitmann dimension of distributive lattices and commutative rings. (Dimension de Heitmann des treillis distributifs et des anneaux commutatifs.) Zbl 1158.13308 Coquand, Thierry; Lombardi, Henri; Quitté, Claude 12 2006 Stack semantics of type theory. Zbl 1452.03037 Coquand, Thierry; Mannaa, Bassel; Ruch, Fabian 11 2017 A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228 Coquand, Thierry; Siles, Vincent 11 2011 Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 1496.06018 Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan 11 2019 The independence of Markov’s principle in type theory. Zbl 1434.03137 Coquand, Thierry; Mannaa, Bassel 10 2016 Towards constructive homological algebra in type theory. Zbl 1202.68376 Coquand, Thierry; Spiwack, Arnaud 10 2007 Formal topologies on the set of first-order formulae. Zbl 0965.03072 Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M. 10 2000 Geometric Hahn–Banach theorem. Zbl 1095.46046 Coquand, Thierry 9 2006 Isomorphism is equality. Zbl 1359.03010 Coquand, Thierry; Danielsson, Nils Anders 9 2013 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049 Coquand, T.; Spitters, B. 9 2005 An intuitionistic proof of Tychonoff’s theorem. Zbl 0764.03024 Coquand, Thierry 9 1992 The univalence axiom in cubical sets. Zbl 1506.03064 Bezem, Marc; Coquand, Thierry; Huber, Simon 9 2019 Canonicity and normalization for dependent type theory. Zbl 1454.03019 Coquand, Thierry 9 2019 On seminormality. Zbl 1102.13005 Coquand, Thierry 8 2006 An equational presentation of higher order logic. Zbl 0643.03050 Coquand, Thierry; Ehrhard, Thomas 8 1987 Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768 Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David 8 2012 Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005 Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 8 2017 Gröbner bases in type theory. Zbl 0979.03044 Coquand, Thierry; Persson, Henrik 8 1999 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052 Coquand, Thierry; Spitters, Bas 8 2009 The Hahn-Banach theorem in type theory. Zbl 0940.03069 Cederquist, Jan; Coquand, Thierry; Negri, Sara 8 1998 Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007 Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude 8 2009 \(A\)-translation and looping combinators in pure type systems. Zbl 0817.03007 Coquand, Thierry; Herbelin, Hugo 8 1994 Compact spaces and distributive lattices. Zbl 1034.54005 Coquand, Thierry 7 2003 A Kripke model for simplicial sets. Zbl 1350.18020 Bezem, Marc; Coquand, Thierry 7 2015 The projective spectrum as a distributive lattice. Zbl 1131.03035 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 7 2007 Homotopy canonicity for cubical type theory. Zbl 1528.03106 Coquand, Thierry; Huber, Simon; Sattler, Christian 7 2019 A computational interpretation of forcing in type theory. Zbl 1312.03021 Coquand, Thierry; Jaber, Guilhem 7 2012 Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Zbl 0627.03045 Coquand, Thierry; Huet, Gérard 6 1987 A note on forcing and type theory. Zbl 1239.03041 Coquand, Thierry; Jaber, Guilhem 6 2010 Non-constructivity in Kan simplicial sets. Zbl 1433.03154 Bezem, Marc; Coquand, Thierry; Parmann, Erik 6 2015 Two applications of Boolean models. Zbl 0904.03026 Coquand, Thierry 6 1998 Generalizations of Hedberg’s theorem. Zbl 1433.03032 Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 6 2013 Recursive functions and constructive mathematics. Zbl 1342.03043 Coquand, Thierry 6 2014 Games with 1-backtracking. Zbl 1241.03006 Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu 6 2010 Syntax and models of Cartesian cubical type theory. Zbl 1529.03123 Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 6 2021 Metric Boolean algebras and constructive measure theory. Zbl 1064.03039 Coquand, Thierry; Palmgren, Erik 5 2002 On a theorem of Kronecker about algebraic varieties. (Sur un théorème de Kronecker concernant les variétés algébriques.) Zbl 1039.13002 Coquand, Thierry 5 2004 A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301 Coquand, Thierry; Lombardi, Henri 5 2005 A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020 Altenkirch, Thorsten; Coquand, Thierry 5 2001 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 Une preuve directe du théorème d’ultime obstination. (A direct proof of the ultimate obstination theorem). Zbl 0749.68052 Coquand, Thierry 5 1992 Spectral schemes as ringed lattices. Zbl 1254.03114 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2009 Type theory and programming. Zbl 0791.68017 Coquand, Thierry; Nordström, Bengt; Smith, Jan M.; von Sydow, Björn 5 1994 A nilregular element property. Zbl 1093.03035 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2005 A new paradox in type theory. Zbl 0821.03005 Coquand, Thierry 5 1994 A representation of stably compact spaces, and patch topology. Zbl 1049.54027 Coquand, Thierry; Zhang, Guo-Qiang 4 2003 A completeness proof for geometrical logic. Zbl 1101.03026 Coquand, Thierry 4 2005 Computing persistent homology within Coq/SSReflect. Zbl 1353.68251 Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 4 2013 Theory of dependent types and axiom of univalence. (Théorie des types dépendants et axiome d’univalence.) Zbl 1356.03002 Coquand, Thierry 4 2015 Intuitionistic choice and classical logic. Zbl 0947.03078 Coquand, Thierry; Palmgren, Erik 4 2000 A proof of strong normalisation using domain theory. Zbl 1131.68038 Coquand, Thierry; Spiwack, Arnaud 4 2007 A proof-theoretical investigation of Zantema’s problem. Zbl 0910.03033 Coquand, Thierry; Persson, Henrik 4 1998 Minimal invariant spaces in formal topology. Zbl 0884.03058 Coquand, Thierry 4 1997 Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324 Bezem, Marc; Coquand, Thierry 4 2003 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2009 On the definition of reduction for infinite terms. Zbl 0859.68049 Coquand, Catarina; Coquand, Thierry 4 1996 A logical framework with dependently typed records. Zbl 1095.03017 Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 4 2005 Constructive finite free resolutions. Zbl 1239.13022 Coquand, Thierry; Quitté, Claude 4 2012 An application of constructive completeness. Zbl 1434.03098 Coquand, Thierry; Smith, Jan M. 4 1996 The independence of Markov’s principle in type theory. Zbl 1434.03136 Coquand, Thierry; Mannaa, Bassel 4 2017 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005 Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2011 A logical framework with dependently typed records. Zbl 1052.68018 Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 3 2003 An introduction to dependent type theory. Zbl 1065.68025 Barthe, Gilles; Coquand, Thierry 3 2002 Canonicity and homotopy canonicity for cubical type theory. Zbl 1486.03027 Coquand, Thierry; Huber, Simon; Sattler, Christian 1 2022 Syntax and models of Cartesian cubical type theory. Zbl 1529.03123 Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 6 2021 Constructive sheaf models of type theory. Zbl 1529.18006 Coquand, Thierry; Ruch, Fabian; Sattler, Christian 2 2021 Lorenzen’s proof of consistency for elementary number theory. Zbl 1512.03073 Coquand, Thierry; Neuwirth, Stefan 3 2020 Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 1528.03099 Abel, Andreas; Coquand, Thierry 3 2020 Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 1496.06018 Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan 11 2019 The univalence axiom in cubical sets. Zbl 1506.03064 Bezem, Marc; Coquand, Thierry; Huber, Simon 9 2019 Canonicity and normalization for dependent type theory. Zbl 1454.03019 Coquand, Thierry 9 2019 Homotopy canonicity for cubical type theory. Zbl 1528.03106 Coquand, Thierry; Huber, Simon; Sattler, Christian 7 2019 Skolem’s theorem in coherent logic. Zbl 1458.03047 Bezem, Marc; Coquand, Thierry 1 2019 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036 Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 85 2018 On higher inductive types in cubical type theory. Zbl 1452.03036 Coquand, Thierry; Huber, Simon; Mörtberg, Anders 27 2018 Syntactic forcing models for coherent logic. Zbl 1437.03188 Bezem, Marc; Buchholtz, Ulrik; Coquand, Thierry 1 2018 Stack semantics of type theory. Zbl 1452.03037 Coquand, Thierry; Mannaa, Bassel; Ruch, Fabian 11 2017 Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005 Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 8 2017 The independence of Markov’s principle in type theory. Zbl 1434.03136 Coquand, Thierry; Mannaa, Bassel 4 2017 Type theory and formalisation of mathematics. Zbl 1489.68395 Coquand, Thierry 1 2017 The independence of Markov’s principle in type theory. Zbl 1434.03137 Coquand, Thierry; Mannaa, Bassel 10 2016 Rings with divisors and Krull rings (a constructive approach). (Anneaux à diviseurs et anneaux de Krull (une approche constructive).) Zbl 1343.13019 Coquand, T.; Lombardi, H. 1 2016 A presheaf model of parametric type theory. Zbl 1351.68146 Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem 15 2015 A Kripke model for simplicial sets. Zbl 1350.18020 Bezem, Marc; Coquand, Thierry 7 2015 Non-constructivity in Kan simplicial sets. Zbl 1433.03154 Bezem, Marc; Coquand, Thierry; Parmann, Erik 6 2015 Theory of dependent types and axiom of univalence. (Théorie des types dépendants et axiome d’univalence.) Zbl 1356.03002 Coquand, Thierry 4 2015 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005 Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 A model of type theory in cubical sets. Zbl 1359.03009 Bezem, Marc; Coquand, Thierry; Huber, Simon 70 2014 Recursive functions and constructive mathematics. Zbl 1342.03043 Coquand, Thierry 6 2014 Revisiting Zariski main theorem from a constructive point of view. Zbl 1391.13049 Alonso, M. E.; Coquand, T.; Lombardi, H. 3 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002 The Univalent Foundations Program 254 2013 Isomorphism is equality. Zbl 1359.03010 Coquand, Thierry; Danielsson, Nils Anders 9 2013 Generalizations of Hedberg’s theorem. Zbl 1433.03032 Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 6 2013 Computing persistent homology within Coq/SSReflect. Zbl 1353.68251 Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 4 2013 Dynamic Newton-Puiseux theorem. Zbl 1345.03115 Mannaa, Bassel; Coquand, Thierry 3 2013 About Goodman’s theorem. Zbl 1284.03267 Coquand, Thierry 3 2013 Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768 Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David 8 2012 A computational interpretation of forcing in type theory. Zbl 1312.03021 Coquand, Thierry; Jaber, Guilhem 7 2012 Constructive finite free resolutions. Zbl 1239.13022 Coquand, Thierry; Quitté, Claude 4 2012 Coherent and strongly discrete rings in type theory. Zbl 1383.03016 Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 2 2012 A formal proof of Sasaki-Murao algorithm. Zbl 1451.68321 Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 2 2012 A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228 Coquand, Thierry; Siles, Vincent 11 2011 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2011 Metric complements of overt closed sets. Zbl 1251.03084 Coquand, Thierry; Palmgren, Erik; Spitters, Bas 2 2011 Unique paths as formal points. Zbl 1296.03036 Coquand, Thierry; Schuster, Peter 1 2011 A note on forcing and type theory. Zbl 1239.03041 Coquand, Thierry; Jaber, Guilhem 6 2010 Games with 1-backtracking. Zbl 1241.03006 Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu 6 2010 Constructively finite? Zbl 1217.03046 Coquand, Thierry; Spiwack, Arnaud 3 2010 Constructive theory of Banach algebras. Zbl 1285.03073 Coquand, Thierry; Spitters, Bas 1 2010 Curves and coherent Prüfer rings. Zbl 1203.13020 Coquand, Thierry; Lombardi, Henri; Quitté, Claude 1 2010 Space of valuations. Zbl 1222.03072 Coquand, Thierry 19 2009 Integrals and valuations. Zbl 1245.03098 Coquand, Thierry; Spitters, Bas 14 2009 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052 Coquand, Thierry; Spitters, Bas 8 2009 Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007 Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude 8 2009 Spectral schemes as ringed lattices. Zbl 1254.03114 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2009 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025 Abel, Andreas; Coquand, Thierry; Pagano, Miguel 4 2009 A simple type-theoretic language: Mini-TT. Zbl 1184.68152 Coquand, Thierry; Kinoshita, Yoshiki; Nordström, Bengt; Takeyama, Makoto 1 2009 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570 Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 A note on the axiomatisation of real numbers. Zbl 1172.03030 Coquand, Thierry; Lombardi, L. Henri 1 2008 Towards constructive homological algebra in type theory. Zbl 1202.68376 Coquand, Thierry; Spiwack, Arnaud 10 2007 The projective spectrum as a distributive lattice. Zbl 1131.03035 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 7 2007 A proof of strong normalisation using domain theory. Zbl 1131.68038 Coquand, Thierry; Spiwack, Arnaud 4 2007 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1121.68026 Abel, Andreas; Coquand, Thierry 1 2007 A logical approach to abstract algebra. Zbl 1118.03059 Coquand, Thierry; Lombardi, Henri 28 2006 Heitmann dimension of distributive lattices and commutative rings. (Dimension de Heitmann des treillis distributifs et des anneaux commutatifs.) Zbl 1158.13308 Coquand, Thierry; Lombardi, Henri; Quitté, Claude 12 2006 Geometric Hahn–Banach theorem. Zbl 1095.46046 Coquand, Thierry 9 2006 On seminormality. Zbl 1102.13005 Coquand, Thierry 8 2006 Formalising bitonic sort in type theory. Zbl 1172.68439 Bove, Ana; Coquand, Thierry 2 2006 Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033 Barthe, Gilles; Coquand, Thierry 2 2006 Automating coherent logic. Zbl 1143.03332 Bezem, Marc; Coquand, Thierry 19 2005 About Stone’s notion of spectrum. Zbl 1061.06031 Coquand, Thierry 18 2005 An elementary characterization of Krull dimension. Zbl 1161.54303 Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise 17 2005 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049 Coquand, T.; Spitters, B. 9 2005 A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301 Coquand, Thierry; Lombardi, Henri 5 2005 A nilregular element property. Zbl 1093.03035 Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2005 A completeness proof for geometrical logic. Zbl 1101.03026 Coquand, Thierry 4 2005 A logical framework with dependently typed records. Zbl 1095.03017 Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 4 2005 Completeness theorems and \(\lambda\)-calculus. Zbl 1112.03307 Coquand, Thierry 3 2005 Connecting a logical framework to a first-order logic prover. Zbl 1171.68712 Abel, Andreas; Coquand, Thierry; Norell, Ulf 2 2005 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1112.68346 Abel, Andreas; Coquand, Thierry 1 2005 Generating non-Noetherian modules constructively. Zbl 1059.13006 Coquand, Thierry; Lombardi, Henri; Quitté, Claude 24 2004 Proof-theoretical analysis of order relations. Zbl 1062.03055 Negri, Sara; von Plato, Jan; Coquand, Thierry 14 2004 On a theorem of Kronecker about algebraic varieties. (Sur un théorème de Kronecker concernant les variétés algébriques.) Zbl 1039.13002 Coquand, Thierry 5 2004 Newman’s lemma – a case study in proof automation and geometric logic. Zbl 1063.68089 Bezem, Marc; Coquand, Thierry 3 2004 A note on measures with values in a partially ordered vector space. Zbl 1065.28006 Coquand, Thierry 2 2004 Inductively generated formal topologies. Zbl 1070.03041 Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio 67 2003 Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507 Coquand, Thierry; Lombardi, Henri 41 2003 Compact spaces and distributive lattices. Zbl 1034.54005 Coquand, Thierry 7 2003 A representation of stably compact spaces, and patch topology. Zbl 1049.54027 Coquand, Thierry; Zhang, Guo-Qiang 4 2003 Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324 Bezem, Marc; Coquand, Thierry 4 2003 A logical framework with dependently typed records. Zbl 1052.68018 Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 3 2003 A syntactical proof of the Marriage Lemma. Zbl 1051.03048 Coquand, Thierry 1 2003 Metric Boolean algebras and constructive measure theory. Zbl 1064.03039 Coquand, Thierry; Palmgren, Erik 5 2002 An introduction to dependent type theory. Zbl 1065.68025 Barthe, Gilles; Coquand, Thierry 3 2002 An implementation of Type:Type. Zbl 1054.68087 Coquand, Thierry; Takeyama, Makoto 2 2002 Valuations and Dedekind’s Prague theorem. Zbl 0983.11061 Coquand, Thierry; Persson, Henrik 21 2001 A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020 Altenkirch, Thorsten; Coquand, Thierry 5 2001 Entailment relations and distributive lattices. Zbl 0948.03056 Cederquist, Jan; Coquand, Thierry 42 2000 Sequents, frames, and completeness. Zbl 0973.03080 Coquand, Thierry; Zhang, Guo-Qiang 12 2000 Formal topologies on the set of first-order formulae. Zbl 0965.03072 Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M. 10 2000 Intuitionistic choice and classical logic. Zbl 0947.03078 Coquand, Thierry; Palmgren, Erik 4 2000 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069 Coquand, Thierry; Hofmann, Martin 15 1999 ...and 41 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 961 Authors 51 Coquand, Thierry 27 Lombardi, Henri 21 Schuster, Peter Michael 17 Spitters, Bas 16 Wessel, Daniel 14 Dybjer, Peter 14 Yengui, Ihsen 13 Berardi, Stefano 12 Altenkirch, Thorsten 12 Sambin, Giovanni 11 Valentini, Silvio 10 Abel, Andreas M. 10 Harper, Robert 10 Rinaldi, Davide 9 Ciraulo, Francesco 9 Hötzel Escardó, Martín 9 Pitts, Andrew M. 8 Buchholtz, Ulrik 8 Huber, Simon 8 Kraus, Nicolai 8 Luo, Zhaohui 8 Pfenning, Frank 8 Rubio García, Julio Jesús 8 Sattler, Christian 8 Veltri, Niccolò 7 Ahrens, Benedikt 7 Angiuli, Carlo 7 Ducos, Lionel 7 Gambino, Nicola 7 Ghani, Neil 7 Vickers, Steven 7 Wadler, Philip Lee 6 Aransay, Jesús 6 Aschieri, Federico 6 Avigad, Jeremy 6 Awodey, Steve 6 Barbanera, Franco 6 Bezem, Marc 6 Curi, Giovanni 6 Curien, Pierre-Louis 6 Dufourd, Jean-François 6 Hendriks, Dimitri 6 Janičić, Predrag 6 Kaposi, Ambrus 6 Kawai, Tatsuji 6 Licata, Daniel R. 6 Maietti, Maria Emilia 6 Møgelberg, Rasmus Ejlers 6 Mörtberg, Anders 6 Nordvall Forsberg, Fredrik 6 Oliva, Paulo 6 Quitté, Claude 6 Rabe, Florian 6 Shulman, Michael A. 6 Uustalu, Tarmo 5 Barthe, Gilles 5 Berger, Ulrich 5 Birkedal, Lars 5 Bove, Ana 5 Chapman, James T. E. 5 de’Liguoro, Ugo 5 Devriese, Dominique 5 Dowek, Gilles 5 Dyckhoff, Roy 5 Endrullis, Jörg 5 Farmer, William M. 5 Kamareddine, Fairouz D. 5 Negri, Sara 5 Neuwirth, Stefan 5 Nuyts, Andreas 5 Orton, Ian 5 Palmgren, Erik 5 Petrakis, Iosif 5 Rathjen, Michael 5 Seldin, Jonathan P. 5 Streicher, Thomas 5 Stump, Aaron 5 van der Weide, Niels 5 Weirich, Stephanie 5 Zhang, Guo-Qiang 4 Abramsky, Samson 4 Blanqui, Frédéric 4 Capretta, Venanzio 4 Cohen, Liron 4 Constable, Robert Lee 4 Domínguez, César 4 Duggan, Dominic 4 Felty, Amy P. 4 Geuvers, Jan Herman 4 Ghelli, Giorgio 4 Gratzer, Daniel 4 Hayashi, Susumu 4 Henry, Simon 4 Heunen, Chris 4 Honsell, Furio 4 Hyland, J. Martin E. 4 Jung, Achim 4 Kohlenbach, Ulrich Wilhelm 4 Landsman, Nicolaas P. 4 Liquori, Luigi ...and 861 more Authors all top 5 Cited in 112 Serials 111 Theoretical Computer Science 77 Annals of Pure and Applied Logic 61 Mathematical Structures in Computer Science 41 Logical Methods in Computer Science 38 Information and Computation 37 Journal of Automated Reasoning 28 Journal of Functional Programming 22 Journal of Algebra 21 The Journal of Symbolic Logic 15 Journal of Symbolic Computation 14 Journal of Pure and Applied Algebra 12 Formal Aspects of Computing 12 Archive for Mathematical Logic 8 Mathematical Logic Quarterly (MLQ) 8 The Bulletin of Symbolic Logic 7 Studia Logica 7 Synthese 7 Annals of Mathematics and Artificial Intelligence 5 The Journal of Logic and Algebraic Programming 5 Journal of Logical and Algebraic Methods in Programming 4 Indagationes Mathematicae. New Series 4 Journal of Applied Logic 4 Foundations of Physics 4 Higher Structures 3 Acta Informatica 3 Communications in Algebra 3 Communications in Mathematical Physics 3 Mathematical Proceedings of the Cambridge Philosophical Society 3 Algebra Universalis 3 Journal of Philosophical Logic 3 Proceedings of the American Mathematical Society 3 Journal of Computer Science and Technology 3 Theory of Computing Systems 3 RAIRO. Theoretical Informatics and Applications 3 Confluentes Mathematici 2 Computers & Mathematics with Applications 2 Information Processing Letters 2 The Mathematical Intelligencer 2 Archiv der Mathematik 2 Mathematische Zeitschrift 2 Notre Dame Journal of Formal Logic 2 Transactions of the American Mathematical Society 2 Bulletin of the Section of Logic 2 Pattern Recognition 2 Bulletin of the American Mathematical Society. New Series 2 RAIRO. Informatique Théorique et Applications 2 Applicable Algebra in Engineering, Communication and Computing 2 Applied Categorical Structures 2 Diagrammes 2 Theory and Applications of Categories 2 Proceedings of the Royal Society of London. Series A. Mathematical, Physical and Engineering Sciences 2 Comptes Rendus. Mathématique. Académie des Sciences, Paris 2 Computer Languages, Systems & Structures 2 ACM Transactions on Computational Logic 2 Oberwolfach Reports 2 Journal of Commutative Algebra 2 Journal of Logic and Analysis 1 Journal of Mathematical Physics 1 Mathematical Methods in the Applied Sciences 1 Rocky Mountain Journal of Mathematics 1 Mathematics of Computation 1 Collectanea Mathematica 1 Czechoslovak Mathematical Journal 1 Dissertationes Mathematicae 1 Fundamenta Mathematicae 1 Fuzzy Sets and Systems 1 Information Sciences 1 Publications Mathématiques 1 Journal of the London Mathematical Society. Second Series 1 Linguistics and Philosophy 1 Manuscripta Mathematica 1 Mathematische Nachrichten 1 Mathematica Scandinavica 1 Pacific Journal of Mathematics 1 Programming and Computer Software 1 Rendiconti dell’Istituto di Matematica dell’Università di Trieste 1 Topology and its Applications 1 Mathematical Social Sciences 1 History and Philosophy of Logic 1 Acta Applicandae Mathematicae 1 Order 1 MCSS. Mathematics of Control, Signals, and Systems 1 Journal of Integral Equations and Applications 1 Computational Geometry 1 International Journal of Algebra and Computation 1 International Journal of Computer Mathematics 1 Linear Algebra and its Applications 1 Journal of Logic, Language and Information 1 Journal of Applied Non-Classical Logics 1 Turkish Journal of Mathematics 1 Advances in Applied Clifford Algebras 1 Filomat 1 The New York Journal of Mathematics 1 Selecta Mathematica. New Series 1 Topoi 1 Higher-Order and Symbolic Computation 1 Fundamenta Informaticae 1 Journal of the Australian Mathematical Society 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 Hacettepe Journal of Mathematics and Statistics ...and 12 more Serials all top 5 Cited in 38 Fields 652 Mathematical logic and foundations (03-XX) 570 Computer science (68-XX) 140 Category theory; homological algebra (18-XX) 88 Order, lattices, ordered algebraic structures (06-XX) 76 Commutative algebra (13-XX) 70 Algebraic topology (55-XX) 45 General topology (54-XX) 23 Algebraic geometry (14-XX) 15 Functional analysis (46-XX) 12 \(K\)-theory (19-XX) 11 History and biography (01-XX) 11 Associative rings and algebras (16-XX) 11 Quantum theory (81-XX) 11 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 10 General and overarching topics; collections (00-XX) 10 Combinatorics (05-XX) 8 Measure and integration (28-XX) 7 General algebraic systems (08-XX) 5 Linear and multilinear algebra; matrix theory (15-XX) 5 Numerical analysis (65-XX) 4 Number theory (11-XX) 4 Field theory and polynomials (12-XX) 4 Operator theory (47-XX) 3 Real functions (26-XX) 3 Geometry (51-XX) 2 Group theory and generalizations (20-XX) 2 Partial differential equations (35-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Convex and discrete geometry (52-XX) 2 Biology and other natural sciences (92-XX) 2 Information and communication theory, circuits (94-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Sequences, series, summability (40-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Integral transforms, operational calculus (44-XX) 1 Integral equations (45-XX) 1 Relativity and gravitational theory (83-XX) 1 Systems theory; control (93-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.