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 Documents Indexed: 170 Publications since 1984 7 Contributions as Editor · 1 Further Contribution Reviewing Activity: 34 Reviews Co-Authors: 78 Co-Authors with 131 Joint Publications 1,138 Co-Co-Authors all top 5 Co-Authors 45 single-authored 19 Lombardi, Henri 14 Bezem, Marc 8 Abel, Andreas M. 8 Huber, Simon 8 Spitters, Bas 7 Dybjer, Peter 6 Schuster, Peter Michael 5 Breazu-Tannen, Val 5 Gunter, Carl A. 5 Mannaa, Bassel 5 Mörtberg, Anders 5 Palmgren, Erik 5 Quitté, Claude 5 Sambin, Giovanni 5 Smith, Jan M. 4 Altenkirch, Thorsten 4 Hötzel Escardó, Martín 4 Huet, Gerard P. 4 Neuwirth, Stefan 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 Sattler, Christian 3 Scedrov, Andre 3 Spiwack, Arnaud 2 Angiuli, Carlo 2 Barras, Bruno 2 Bauer, Andrej 2 Brunerie, Guillaume 2 Cederquist, Jan 2 Dawar, Anuj 2 Harper, Robert 2 Herbelin, Hugo 2 Hofmann, Martin 2 Hou (Favonia), Kuen-Bang 2 Jaber, Guilhem 2 Maietti, Maria Emilia 2 Negri, Sara 2 Pagano, Miguel 2 Pollack, Randy 2 Quadrat, Alban 2 Ruch, Fabian 2 Winskel, Glynn 1 Aczel, Peter 1 Ahrens, Benedikt 1 Alonso García, María Emilia 1 Avigad, Jeremy 1 Awodey, Steve 1 Banaschewski, Bernhard 1 Barakat, Mohamed 1 Bernardy, Jean-Philippe 1 Bertot, Yves 1 Bordg, Anthony 1 Bove, Ana 1 Buchholtz, Ulrik 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 1 Polonsky, Andrew 1 Riehl, Emily 1 Rijke, Egbert 1 Roy, Marie-Françoise 1 Sadocco, Sara 1 Scott, Dana Stewart ...and 19 more Co-Authors all top 5 Serials 8 Theoretical Computer Science 8 Annals of Pure and Applied Logic 7 MSCS. 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 145 Mathematical logic and foundations (03-XX) 67 Computer science (68-XX) 26 Commutative algebra (13-XX) 24 Order, lattices, ordered algebraic structures (06-XX) 15 Category theory; homological algebra (18-XX) 12 General topology (54-XX) 10 Algebraic topology (55-XX) 9 General and overarching topics; collections (00-XX) 9 Algebraic geometry (14-XX) 6 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) 1 General algebraic systems (08-XX) 1 Number theory (11-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Associative rings and algebras (16-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 133 Publications have been cited 1,329 times in 833 Documents Cited by ▼ Year ▼ The calculus of constructions. Zbl 0654.03045Coquand, Thierry; Huet, Gérard 181 1988 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 Inductively generated formal topologies. Zbl 1070.03041Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio 64 2003 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 58 2018 A model of type theory in cubical sets. Zbl 1359.03009Bezem, Marc; Coquand, Thierry; Huber, Simon 55 2014 Entailment relations and distributive lattices. Zbl 0948.03056Cederquist, Jan; Coquand, Thierry 38 2000 Inductively defined types. Zbl 0722.03006Coquand, Thierry; Paulin, Christine 37 1990 Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507Coquand, Thierry; Lombardi, Henri 36 2003 Constructions: A higher order proof system for mechanizing mathematics. Zbl 0581.03007Coquand, Thierry; Huet, Gérard 35 1985 A semantics of evidence for classical arithmetic. Zbl 0829.03037Coquand, Thierry 33 1995 On the computational content of the axiom of choice. Zbl 0914.03059Berardi, Stefano; Bezem, Marc; Coquand, Thierry 28 1998 Domain theoretic models of polymorphism. Zbl 0683.03007Coquand, Thierry; Gunter, Carl; Winskel, Glynn 27 1989 Inheritance as implicit coercion. Zbl 0799.68129Breazu-Tannen, Val; Coquand, Thierry; Gunter, Carl A.; Scedrov, Andre 26 1991 A logical approach to abstract algebra. Zbl 1118.03059Coquand, Thierry; Lombardi, Henri 25 2006 Generating non-Noetherian modules constructively. Zbl 1059.13006Coquand, Thierry; Lombardi, Henri; Quitté, Claude 23 2004 An algorithm for testing conversion in type theory. Zbl 0754.03041Coquand, Thierry 21 1991 On higher inductive types in cubical type theory. Zbl 1452.03036Coquand, Thierry; Huber, Simon; Mörtberg, Anders 18 2018 Intuitionistic model constructions and normalization proofs. Zbl 0883.03009Coquand, Thierry; Dybjer, Peter 18 1997 Valuations and Dedekind’s Prague theorem. Zbl 0983.11061Coquand, Thierry; Persson, Henrik 17 2001 About Stone’s notion of spectrum. Zbl 1061.06031Coquand, Thierry 16 2005 Automating coherent logic. Zbl 1143.03332Bezem, Marc; Coquand, Thierry 15 2005 An elementary characterization of Krull dimension. Zbl 1161.54303Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise 14 2005 Extensional models for polymorphism. Zbl 0713.03005Breazu-Tannen, Val; Coquand, Thierry 14 1988 Space of valuations. Zbl 1222.03072Coquand, Thierry 13 2009 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069Coquand, Thierry; Hofmann, Martin 13 1999 Proof-theoretical analysis of order relations. Zbl 1062.03055Negri, Sara; von Plato, Jan; Coquand, Thierry 13 2004 Inheritance and explicit coercion. Zbl 0716.68012Breazu-Tannen, V.; Coquand, T.; Gunter, C. A.; Scedrov, A. 12 1989 Integrals and valuations. Zbl 1245.03098Coquand, Thierry; Spitters, Bas 12 2009 Categories of embeddings. Zbl 0688.18004Coquand, Thierry 12 1989 An algorithm for type-checking dependent types. Zbl 0853.68102Coquand, Thierry 10 1996 Constructive topology and combinatorics. Zbl 1434.03143Coquand, Thierry 10 1992 A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228Coquand, Thierry; Siles, Vincent 10 2011 Heitmann dimension of distributive lattices and commutative rings. (Dimension de Heitmann des treillis distributifs et des anneaux commutatifs.) Zbl 1158.13308Coquand, Thierry; Lombardi, Henri; Quitté, Claude 10 2006 Formal topologies on the set of first-order formulae. Zbl 0965.03072Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M. 10 2000 Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 1496.06018Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan 10 2019 Sequents, frames, and completeness. Zbl 0973.03080Coquand, Thierry; Zhang, Guo-Qiang 9 2000 An intuitionistic proof of Tychonoff’s theorem. Zbl 0764.03024Coquand, Thierry 9 1992 Geometric Hahn–Banach theorem. Zbl 1095.46046Coquand, Thierry 9 2006 A presheaf model of parametric type theory. Zbl 1351.68146Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem 9 2015 Stack semantics of type theory. Zbl 1452.03037Coquand, Thierry; Mannaa, Bassel; Ruch, Fabian 8 2017 \(A\)-translation and looping combinators in pure type systems. Zbl 0817.03007Coquand, Thierry; Herbelin, Hugo 8 1994 The independence of Markov’s principle in type theory. Zbl 1434.03137Coquand, Thierry; Mannaa, Bassel 8 2016 On seminormality. Zbl 1102.13005Coquand, Thierry 8 2006 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049Coquand, T.; Spitters, B. 8 2005 Towards constructive homological algebra in type theory. Zbl 1202.68376Coquand, Thierry; Spiwack, Arnaud 8 2007 Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude 8 2009 dI-domains as a model of polymorphism. Zbl 0644.68041Coquand, Thierry; Gunter, Carl; Winskel, Glynn 8 1988 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 The Hahn-Banach theorem in type theory. Zbl 0940.03069Cederquist, Jan; Coquand, Thierry; Negri, Sara 7 1998 Canonicity and normalization for dependent type theory. Zbl 1454.03019Coquand, Thierry 7 2019 Isomorphism is equality. Zbl 1359.03010Coquand, Thierry; Danielsson, Nils Anders 7 2013 A Kripke model for simplicial sets. Zbl 1350.18020Bezem, Marc; Coquand, Thierry 7 2015 The projective spectrum as a distributive lattice. Zbl 1131.03035Coquand, Thierry; Lombardi, Henri; Schuster, Peter 7 2007 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052Coquand, Thierry; Spitters, Bas 7 2009 Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David 7 2012 The univalence axiom in cubical sets. Zbl 1506.03064Bezem, Marc; Coquand, Thierry; Huber, Simon 7 2019 Compact spaces and distributive lattices. Zbl 1034.54005Coquand, Thierry 6 2003 Recursive functions and constructive mathematics. Zbl 1342.03043Coquand, Thierry 6 2014 A computational interpretation of forcing in type theory. Zbl 1312.03021Coquand, Thierry; Jaber, Guilhem 6 2012 Two applications of Boolean models. Zbl 0904.03026Coquand, Thierry 6 1998 Non-constructivity in Kan simplicial sets. Zbl 1433.03154Bezem, Marc; Coquand, Thierry; Parmann, Erik 6 2015 Games with 1-backtracking. Zbl 1241.03006Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu 6 2010 A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020Altenkirch, Thorsten; Coquand, Thierry 5 2001 A new paradox in type theory. Zbl 0821.03005Coquand, Thierry 5 1994 A nilregular element property. Zbl 1093.03035Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2005 Une preuve directe du théorème d’ultime obstination. (A direct proof of the ultimate obstination theorem). Zbl 0749.68052Coquand, Thierry 5 1992 A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301Coquand, Thierry; Lombardi, Henri 5 2005 Gröbner bases in type theory. Zbl 0979.03044Coquand, Thierry; Persson, Henrik 5 1999 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 Spectral schemes as ringed lattices. Zbl 1254.03114Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2009 Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 5 2017 On a theorem of Kronecker about algebraic varieties. (Sur un théorème de Kronecker concernant les variétés algébriques.) Zbl 1039.13002Coquand, Thierry 5 2004 An application of constructive completeness. Zbl 1434.03098Coquand, Thierry; Smith, Jan M. 4 1996 On the definition of reduction for infinite terms. Zbl 0859.68049Coquand, Catarina; Coquand, Thierry 4 1996 A proof-theoretical investigation of Zantema’s problem. Zbl 0910.03033Coquand, Thierry; Persson, Henrik 4 1998 Metric Boolean algebras and constructive measure theory. Zbl 1064.03039Coquand, Thierry; Palmgren, Erik 4 2002 Minimal invariant spaces in formal topology. Zbl 0884.03058Coquand, Thierry 4 1997 A logical framework with dependently typed records. Zbl 1095.03017Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 4 2005 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 Computing persistent homology within Coq/SSReflect. Zbl 1353.68251Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 4 2013 A note on forcing and type theory. Zbl 1239.03041Coquand, Thierry; Jaber, Guilhem 4 2010 Intuitionistic choice and classical logic. Zbl 0947.03078Coquand, Thierry; Palmgren, Erik 4 2000 A proof of strong normalisation using domain theory. Zbl 1131.68038Coquand, Thierry; Spiwack, Arnaud 4 2007 Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Zbl 0627.03045Coquand, Thierry; Huet, Gérard 4 1987 An equational presentation of higher order logic. Zbl 0643.03050Coquand, Thierry; Ehrhard, Thomas 4 1987 Constructive finite free resolutions. Zbl 1239.13022Coquand, Thierry; Quitté, Claude 4 2012 Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324Bezem, Marc; Coquand, Thierry 4 2003 Generalizations of Hedberg’s theorem. Zbl 1433.03032Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 4 2013 Syntax and models of Cartesian cubical type theory. Zbl 07460116Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 4 2021 A representation of stably compact spaces, and patch topology. Zbl 1049.54027Coquand, Thierry; Zhang, Guo-Qiang 4 2003 An analysis of Ramsey’s theorem. Zbl 0824.03034Coquand, Thierry 3 1994 Revisiting Zariski main theorem from a constructive point of view. Zbl 1391.13049Alonso, M. E.; Coquand, T.; Lombardi, H. 3 2014 Completeness theorems and \(\lambda\)-calculus. Zbl 1112.03307Coquand, Thierry 3 2005 Theory of dependent types and axiom of univalence. (Théorie des types dépendants et axiome d’univalence.) Zbl 1356.03002Coquand, Thierry 3 2015 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199Abel, Andreas; Coquand, Thierry; Pagano, Miguel 3 2011 About Goodman’s theorem. Zbl 1284.03267Coquand, Thierry 3 2013 Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 07225974Abel, Andreas; Coquand, Thierry 2 2020 Dynamic Newton-Puiseux theorem. Zbl 1345.03115Mannaa, Bassel; Coquand, Thierry 2 2013 Type theory and programming. Zbl 0791.68017Coquand, Thierry; Nordström, Bengt; Smith, Jan M.; von Sydow, Björn 2 1994 Computational content of classical logic. Zbl 0916.03035Coquand, Thierry 2 1997 Syntax and models of Cartesian cubical type theory. Zbl 07460116Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 4 2021 Constructive sheaf models of type theory. Zbl 07547339Coquand, Thierry; Ruch, Fabian; Sattler, Christian 1 2021 Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Zbl 07225974Abel, Andreas; Coquand, Thierry 2 2020 Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 1496.06018Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan 10 2019 Canonicity and normalization for dependent type theory. Zbl 1454.03019Coquand, Thierry 7 2019 The univalence axiom in cubical sets. Zbl 1506.03064Bezem, Marc; Coquand, Thierry; Huber, Simon 7 2019 Homotopy canonicity for cubical type theory. Zbl 07559277Coquand, Thierry; Huber, Simon; Sattler, Christian 2 2019 Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders 58 2018 On higher inductive types in cubical type theory. Zbl 1452.03036Coquand, Thierry; Huber, Simon; Mörtberg, Anders 18 2018 Syntactic forcing models for coherent logic. Zbl 1437.03188Bezem, Marc; Buchholtz, Ulrik; Coquand, Thierry 1 2018 Stack semantics of type theory. Zbl 1452.03037Coquand, Thierry; Mannaa, Bassel; Ruch, Fabian 8 2017 Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 5 2017 The independence of Markov’s principle in type theory. Zbl 1434.03136Coquand, Thierry; Mannaa, Bassel 2 2017 Type theory and formalisation of mathematics. Zbl 1489.68395Coquand, Thierry 1 2017 The independence of Markov’s principle in type theory. Zbl 1434.03137Coquand, Thierry; Mannaa, Bassel 8 2016 A presheaf model of parametric type theory. Zbl 1351.68146Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem 9 2015 A Kripke model for simplicial sets. Zbl 1350.18020Bezem, Marc; Coquand, Thierry 7 2015 Non-constructivity in Kan simplicial sets. Zbl 1433.03154Bezem, Marc; Coquand, Thierry; Parmann, Erik 6 2015 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 Theory of dependent types and axiom of univalence. (Théorie des types dépendants et axiome d’univalence.) Zbl 1356.03002Coquand, Thierry 3 2015 A model of type theory in cubical sets. Zbl 1359.03009Bezem, Marc; Coquand, Thierry; Huber, Simon 55 2014 Recursive functions and constructive mathematics. Zbl 1342.03043Coquand, Thierry 6 2014 Revisiting Zariski main theorem from a constructive point of view. Zbl 1391.13049Alonso, M. E.; Coquand, T.; Lombardi, H. 3 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 Isomorphism is equality. Zbl 1359.03010Coquand, Thierry; Danielsson, Nils Anders 7 2013 Computing persistent homology within Coq/SSReflect. Zbl 1353.68251Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 4 2013 Generalizations of Hedberg’s theorem. Zbl 1433.03032Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten 4 2013 About Goodman’s theorem. Zbl 1284.03267Coquand, Thierry 3 2013 Dynamic Newton-Puiseux theorem. Zbl 1345.03115Mannaa, Bassel; Coquand, Thierry 2 2013 Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David 7 2012 A computational interpretation of forcing in type theory. Zbl 1312.03021Coquand, Thierry; Jaber, Guilhem 6 2012 Constructive finite free resolutions. Zbl 1239.13022Coquand, Thierry; Quitté, Claude 4 2012 Coherent and strongly discrete rings in type theory. Zbl 1383.03016Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 2 2012 A formal proof of Sasaki-Murao algorithm. Zbl 1451.68321Coquand, Thierry; Mörtberg, Anders; Siles, Vincent 1 2012 A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228Coquand, Thierry; Siles, Vincent 10 2011 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199Abel, Andreas; Coquand, Thierry; Pagano, Miguel 3 2011 Metric complements of overt closed sets. Zbl 1251.03084Coquand, Thierry; Palmgren, Erik; Spitters, Bas 2 2011 Unique paths as formal points. Zbl 1296.03036Coquand, Thierry; Schuster, Peter 1 2011 Games with 1-backtracking. Zbl 1241.03006Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu 6 2010 A note on forcing and type theory. Zbl 1239.03041Coquand, Thierry; Jaber, Guilhem 4 2010 Constructively finite? Zbl 1217.03046Coquand, Thierry; Spiwack, Arnaud 1 2010 Constructive theory of Banach algebras. Zbl 1285.03073Coquand, Thierry; Spitters, Bas 1 2010 Space of valuations. Zbl 1222.03072Coquand, Thierry 13 2009 Integrals and valuations. Zbl 1245.03098Coquand, Thierry; Spitters, Bas 12 2009 Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude 8 2009 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052Coquand, Thierry; Spitters, Bas 7 2009 Spectral schemes as ringed lattices. Zbl 1254.03114Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2009 A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1246.03025Abel, Andreas; Coquand, Thierry; Pagano, Miguel 2 2009 A simple type-theoretic language: Mini-TT. Zbl 1184.68152Coquand, 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.68025Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 A note on the axiomatisation of real numbers. Zbl 1172.03030Coquand, Thierry; Lombardi, L. Henri 1 2008 Towards constructive homological algebra in type theory. Zbl 1202.68376Coquand, Thierry; Spiwack, Arnaud 8 2007 The projective spectrum as a distributive lattice. Zbl 1131.03035Coquand, Thierry; Lombardi, Henri; Schuster, Peter 7 2007 A proof of strong normalisation using domain theory. Zbl 1131.68038Coquand, Thierry; Spiwack, Arnaud 4 2007 Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1121.68026Abel, Andreas; Coquand, Thierry 1 2007 A logical approach to abstract algebra. Zbl 1118.03059Coquand, Thierry; Lombardi, Henri 25 2006 Heitmann dimension of distributive lattices and commutative rings. (Dimension de Heitmann des treillis distributifs et des anneaux commutatifs.) Zbl 1158.13308Coquand, Thierry; Lombardi, Henri; Quitté, Claude 10 2006 Geometric Hahn–Banach theorem. Zbl 1095.46046Coquand, Thierry 9 2006 On seminormality. Zbl 1102.13005Coquand, Thierry 8 2006 Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033Barthe, Gilles; Coquand, Thierry 2 2006 Formalising bitonic sort in type theory. Zbl 1172.68439Bove, Ana; Coquand, Thierry 1 2006 About Stone’s notion of spectrum. Zbl 1061.06031Coquand, Thierry 16 2005 Automating coherent logic. Zbl 1143.03332Bezem, Marc; Coquand, Thierry 15 2005 An elementary characterization of Krull dimension. Zbl 1161.54303Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise 14 2005 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049Coquand, T.; Spitters, B. 8 2005 A nilregular element property. Zbl 1093.03035Coquand, Thierry; Lombardi, Henri; Schuster, Peter 5 2005 A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301Coquand, Thierry; Lombardi, Henri 5 2005 A logical framework with dependently typed records. Zbl 1095.03017Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 4 2005 Completeness theorems and \(\lambda\)-calculus. Zbl 1112.03307Coquand, Thierry 3 2005 Connecting a logical framework to a first-order logic prover. Zbl 1171.68712Abel, Andreas; Coquand, Thierry; Norell, Ulf 2 2005 A completeness proof for geometrical logic. Zbl 1101.03026Coquand, Thierry 1 2005 Generating non-Noetherian modules constructively. Zbl 1059.13006Coquand, Thierry; Lombardi, Henri; Quitté, Claude 23 2004 Proof-theoretical analysis of order relations. Zbl 1062.03055Negri, Sara; von Plato, Jan; Coquand, Thierry 13 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.13002Coquand, Thierry 5 2004 Newman’s lemma – a case study in proof automation and geometric logic. Zbl 1063.68089Bezem, Marc; Coquand, Thierry 2 2004 A note on measures with values in a partially ordered vector space. Zbl 1065.28006Coquand, Thierry 2 2004 Inductively generated formal topologies. Zbl 1070.03041Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio 64 2003 Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507Coquand, Thierry; Lombardi, Henri 36 2003 Compact spaces and distributive lattices. Zbl 1034.54005Coquand, Thierry 6 2003 Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324Bezem, Marc; Coquand, Thierry 4 2003 A representation of stably compact spaces, and patch topology. Zbl 1049.54027Coquand, Thierry; Zhang, Guo-Qiang 4 2003 A logical framework with dependently typed records. Zbl 1052.68018Coquand, Thierry; Pollack, Randy; Takeyama, Makoto 2 2003 A syntactical proof of the Marriage Lemma. Zbl 1051.03048Coquand, Thierry 1 2003 Metric Boolean algebras and constructive measure theory. Zbl 1064.03039Coquand, Thierry; Palmgren, Erik 4 2002 An implementation of Type:Type. Zbl 1054.68087Coquand, Thierry; Takeyama, Makoto 2 2002 An introduction to dependent type theory. Zbl 1065.68025Barthe, Gilles; Coquand, Thierry 1 2002 Valuations and Dedekind’s Prague theorem. Zbl 0983.11061Coquand, Thierry; Persson, Henrik 17 2001 A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020Altenkirch, Thorsten; Coquand, Thierry 5 2001 Entailment relations and distributive lattices. Zbl 0948.03056Cederquist, Jan; Coquand, Thierry 38 2000 Formal topologies on the set of first-order formulae. Zbl 0965.03072Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M. 10 2000 Sequents, frames, and completeness. Zbl 0973.03080Coquand, Thierry; Zhang, Guo-Qiang 9 2000 Intuitionistic choice and classical logic. Zbl 0947.03078Coquand, Thierry; Palmgren, Erik 4 2000 A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069Coquand, Thierry; Hofmann, Martin 13 1999 Gröbner bases in type theory. Zbl 0979.03044Coquand, Thierry; Persson, Henrik 5 1999 A Boolean model of ultrafilters. Zbl 0930.03042Coquand, Thierry 1 1999 On the computational content of the axiom of choice. Zbl 0914.03059Berardi, Stefano; Bezem, Marc; Coquand, Thierry 28 1998 The Hahn-Banach theorem in type theory. Zbl 0940.03069Cederquist, Jan; Coquand, Thierry; Negri, Sara 7 1998 Two applications of Boolean models. Zbl 0904.03026Coquand, Thierry 6 1998 A proof-theoretical investigation of Zantema’s problem. Zbl 0910.03033Coquand, Thierry; Persson, Henrik 4 1998 ...and 33 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 792 Authors 47 Coquand, Thierry 24 Lombardi, Henri 19 Schuster, Peter Michael 16 Spitters, Bas 15 Wessel, Daniel 14 Dybjer, Peter 13 Berardi, Stefano 13 Yengui, Ihsen 12 Sambin, Giovanni 11 Valentini, Silvio 10 Rinaldi, Davide 9 Ciraulo, Francesco 9 Hötzel Escardó, Martín 8 Abel, Andreas M. 8 Altenkirch, Thorsten 8 Harper, Robert 8 Luo, Zhaohui 7 Ducos, Lionel 7 Huber, Simon 7 Pitts, Andrew M. 7 Rubio García, Julio Jesús 7 Vickers, Steven 6 Angiuli, Carlo 6 Aschieri, Federico 6 Avigad, Jeremy 6 Bezem, Marc 6 Curi, Giovanni 6 Curien, Pierre-Louis 6 Dufourd, Jean-François 6 Ghani, Neil 6 Kawai, Tatsuji 6 Nordvall Forsberg, Fredrik 6 Oliva, Paulo 6 Quitté, Claude 6 Sattler, Christian 5 Ahrens, Benedikt 5 Aransay, Jesús 5 Barbanera, Franco 5 Bove, Ana 5 Buchholtz, Ulrik 5 de’Liguoro, Ugo 5 Dyckhoff, Roy 5 Farmer, William M. 5 Gambino, Nicola 5 Janičić, Predrag 5 Kamareddine, Fairouz D. 5 Kraus, Nicolai 5 Maietti, Maria Emilia 5 Mörtberg, Anders 5 Negri, Sara 5 Palmgren, Erik 5 Pfenning, Frank 5 Rabe, Florian 5 Rathjen, Michael 5 Seldin, Jonathan P. 5 Shulman, Michael A. 5 Veltri, Niccolò 4 Barthe, Gilles 4 Birkedal, Lars 4 Blanqui, Frédéric 4 Dowek, Gilles 4 Duggan, Dominic 4 Felty, Amy P. 4 Hendriks, Dimitri 4 Henry, Simon 4 Heunen, Chris 4 Honsell, Furio 4 Jung, Achim 4 Kaposi, Ambrus 4 Kohlenbach, Ulrich Wilhelm 4 Landsman, Nicolaas P. 4 Licata, Daniel R. 4 Maschio, Samuele 4 Møgelberg, Rasmus Ejlers 4 Nederpelt, Rob 4 Orsanigo, Federico 4 Orton, Ian 4 Polonsky, Andrew 4 Ruiz-Reina, José-Luis 4 Schrijvers, Tom 4 Smolka, Gert 4 Streicher, Thomas 4 Stump, Aaron 4 Tassi, Enrico 4 Wadler, Philip Lee 3 Abramsky, Samson 3 Akama, Yohji 3 Alonso García, María Emilia 3 Awodey, Steve 3 Barhoumi, Sami 3 Berger, Ulrich 3 Bizjak, Aleš 3 Breazu-Tannen, Val 3 Bruce, Kim B. 3 Chapman, James T. E. 3 Clouston, Ranald A. 3 Compagnoni, Adriana B. 3 Constable, Robert Lee 3 Dehlinger, Christophe 3 Domínguez, César ...and 692 more Authors all top 5 Cited in 102 Serials 92 Theoretical Computer Science 72 Annals of Pure and Applied Logic 52 MSCS. Mathematical Structures in Computer Science 36 Logical Methods in Computer Science 34 Information and Computation 34 Journal of Automated Reasoning 23 Journal of Functional Programming 21 Journal of Algebra 21 The Journal of Symbolic Logic 14 Journal of Pure and Applied Algebra 14 Journal of Symbolic Computation 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 6 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 3 Acta Informatica 3 Communications in Algebra 3 Mathematical Proceedings of the Cambridge Philosophical Society 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 Foundations of Physics 3 Confluentes Mathematici 3 Higher Structures 2 Communications in Mathematical Physics 2 The Mathematical Intelligencer 2 Algebra Universalis 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 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 Computers & Mathematics with Applications 1 Information Processing Letters 1 Journal of Mathematical Physics 1 Mathematics of Computation 1 Collectanea Mathematica 1 Dissertationes Mathematicae 1 Fuzzy Sets and Systems 1 Information Sciences 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 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 Advances in Applied Clifford Algebras 1 Filomat 1 The New York Journal of Mathematics 1 Theory and Applications of Categories 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 1 Journal of Algebra and its Applications 1 Mediterranean Journal of Mathematics 1 Electronic Notes in Theoretical Computer Science 1 Logica Universalis 1 Banach Journal of Mathematical Analysis 1 São Paulo Journal of Mathematical Sciences 1 The Review of Symbolic Logic 1 Computability ...and 2 more Serials all top 5 Cited in 38 Fields 548 Mathematical logic and foundations (03-XX) 464 Computer science (68-XX) 108 Category theory; homological algebra (18-XX) 78 Order, lattices, ordered algebraic structures (06-XX) 69 Commutative algebra (13-XX) 41 General topology (54-XX) 41 Algebraic topology (55-XX) 21 Algebraic geometry (14-XX) 14 Functional analysis (46-XX) 11 \(K\)-theory (19-XX) 11 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 10 Combinatorics (05-XX) 10 Associative rings and algebras (16-XX) 10 Quantum theory (81-XX) 9 History and biography (01-XX) 7 General and overarching topics; collections (00-XX) 7 Measure and integration (28-XX) 5 General algebraic systems (08-XX) 5 Numerical analysis (65-XX) 4 Field theory and polynomials (12-XX) 4 Linear and multilinear algebra; matrix theory (15-XX) 4 Operator theory (47-XX) 3 Real functions (26-XX) 2 Number theory (11-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) 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 Geometry (51-XX) 1 Relativity and gravitational theory (83-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-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.