# zbMATH — the first resource for mathematics

## Coquand, Thierry

Compute Distance To:
 Author ID: coquand.thierry Published as: Coquand, T.; Coquand, Thierry Homepage: http://www.cse.chalmers.se/~coquand/ External Links: MGP · Wikidata · ResearchGate · dblp · GND Member of Collective: the-univalent-foundations-program.
 Documents Indexed: 163 Publications since 1984, including 2 Books Reviewing Activity: 34 Reviews
all top 5

#### Co-Authors

 42 single-authored 17 Lombardi, Henri 11 Bezem, Marc 8 Abel, Andreas M. 7 Spitters, Bas 6 Huber, Simon 6 Schuster, Peter Michael 5 Breazu-Tannen, Val 5 Dybjer, Peter 5 Gunter, Carl A. 5 Mörtberg, Anders 5 Quitté, Claude 5 Sambin, Giovanni 5 Smith, Jan M. 4 Huet, Gerard P. 4 Mannaa, Bassel 4 Palmgren, Erik 4 Siles, Vincent 4 Takeyama, Makoto 3 Altenkirch, Thorsten 3 Barthe, Gilles 3 Berardi, Stefano 3 Nordström, Bengt 3 Persson, Henrik 3 Scedrov, Andre 3 Spiwack, Arnaud 2 Cederquist, Jan 2 Cohen, Cyril 2 Dawar, Anuj 2 Hötzel Escardó, Martín 2 Jaber, Guilhem 2 Kraus, Nicolai 2 Maietti, Maria Emilia 2 Negri, Sara 2 Pagano, Miguel 2 Pollack, Randy 2 Quadrat, Alban 2 Winskel, Glynn 2 Zhang, Guoqiang 1 Alonso García, María Emilia 1 Banaschewski, Bernhard 1 Barakat, Mohamed 1 Barras, Bruno 1 Bauer, Andrej 1 Bernardy, Jean-Philippe 1 Bove, Ana 1 Buchholtz, Ulrik 1 Coquand, Catarina 1 Danielsson, Nils Anders 1 Ducos, Lionel 1 Ehrhard, Thomas 1 Hayashi, Susumu 1 Heras, Jónathan 1 Herbelin, Hugo 1 Hofmann, Martin 1 Kinoshita, Yoshiki 1 Moulin, Guilhem 1 Neuwirth, Stefan 1 Niwiński, Damian 1 Norell, Ulf 1 Parmann, Erik 1 Paulin, Christine 1 Roy, Marie-Françoise 1 Ruch, Fabian 1 Sadocco, Sara 1 Stolzenberg, Gabriel 1 Tête, Claire 1 Valentini, Silvio 1 von Plato, Jan 1 von Sydow, Björn 1 Vytiniotis, Dimitrios 1 Wahlstedt, David 1 Yengui, Ihsen
all top 5

#### Serials

 8 Annals of Pure and Applied Logic 7 Theoretical Computer Science 6 Journal of Logic and Analysis 5 The Journal of Symbolic Logic 5 Fundamenta Informaticae 5 Logical Methods in Computer Science 4 Journal of Algebra 4 Journal of Pure and Applied Algebra 4 Information and Computation 4 MSCS. Mathematical Structures in Computer Science 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 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

 129 Mathematical logic and foundations (03-XX) 65 Computer science (68-XX) 26 Commutative algebra (13-XX) 20 Order, lattices, ordered algebraic structures (06-XX) 13 Category theory; homological algebra (18-XX) 13 General topology (54-XX) 9 General and overarching topics; collections (00-XX) 8 Algebraic geometry (14-XX) 6 Functional analysis (46-XX) 6 Algebraic topology (55-XX) 5 Combinatorics (05-XX) 4 History and biography (01-XX) 4 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)

#### Citations contained in zbMATH Open

120 Publications have been cited 994 times in 657 Documents Cited by Year
The calculus of constructions. Zbl 0654.03045
Coquand, Thierry; Huet, Gérard
1988
Inductively generated formal topologies. Zbl 1070.03041
Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio
2003
Constructions: A higher order proof system for mechanizing mathematics. Zbl 0581.03007
Coquand, Thierry; Huet, Gérard
1985
Inductively defined types. Zbl 0722.03006
Coquand, Thierry; Paulin, Christine
1990
A model of type theory in cubical sets. Zbl 1359.03009
Bezem, Marc; Coquand, Thierry; Huber, Simon
2014
Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507
Coquand, Thierry; Lombardi, Henri
2003
A semantics of evidence for classical arithmetic. Zbl 0829.03037
Coquand, Thierry
1995
Domain theoretic models of polymorphism. Zbl 0683.03007
Coquand, Thierry; Gunter, Carl; Winskel, Glynn
1989
Inheritance as implicit coercion. Zbl 0799.68129
Breazu-Tannen, Val; Coquand, Thierry; Gunter, Carl A.; Scedrov, Andre
1991
On the computational content of the axiom of choice. Zbl 0914.03059
Berardi, Stefano; Bezem, Marc; Coquand, Thierry
1998
Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036
Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders
2018
Entailment relations and distributive lattices. Zbl 0948.03056
Cederquist, Jan; Coquand, Thierry
2000
Generating non-Noetherian modules constructively. Zbl 1059.13006
Coquand, Thierry; Lombardi, Henri; Quitté, Claude
2004
A logical approach to abstract algebra. Zbl 1118.03059
Coquand, Thierry; Lombardi, Henri
2006
An algorithm for testing conversion in type theory. Zbl 0754.03041
Coquand, Thierry
1991
About Stone’s notion of spectrum. Zbl 1061.06031
Coquand, Thierry
2005
Valuations and Dedekind’s Prague theorem. Zbl 0983.11061
2001
Automating coherent logic. Zbl 1143.03332
Bezem, Marc; Coquand, Thierry
2005
An elementary characterization of Krull dimension. Zbl 1161.54303
Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise
2005
Intuitionistic model constructions and normalization proofs. Zbl 0883.03009
Coquand, Thierry; Dybjer, Peter
1997
Extensional models for polymorphism. Zbl 0713.03005
Breazu-Tannen, Val; Coquand, Thierry
1988
A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069
Coquand, Thierry; Hofmann, Martin
1999
dI-domains as a model of polymorphism. Zbl 0644.68041
Coquand, Thierry; Gunter, Carl; Winskel, Glynn
1988
Categories of embeddings. Zbl 0688.18004
Coquand, Thierry
1989
Space of valuations. Zbl 1222.03072
Coquand, Thierry
2009
Constructive topology and combinatorics. Zbl 1434.03143
Coquand, Thierry
1992
Integrals and valuations. Zbl 1245.03098
Coquand, Thierry; Spitters, Bas
2009
Formal topologies on the set of first-order formulae. Zbl 0965.03072
Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M.
2000
Inheritance and explicit coercion. Zbl 0716.68012
Breazu-Tannen, V.; Coquand, T.; Gunter, C. A.; Scedrov, A.
1989
A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228
Coquand, Thierry; Siles, Vincent
2011
Constructive Gelfand duality for C$$^*$$-algebras. Zbl 1183.46052
Coquand, Thierry; Spitters, Bas
2009
Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049
Coquand, T.; Spitters, B.
2005
$$A$$-translation and looping combinators in pure type systems. Zbl 0817.03007
Coquand, Thierry; Herbelin, Hugo
1994
An intuitionistic proof of Tychonoff’s theorem. Zbl 0764.03024
Coquand, Thierry
1992
An equational presentation of higher order logic. Zbl 0643.03050
Coquand, Thierry; Ehrhard, Thomas
1987
Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007
Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude
2009
Verifying a semantic $$\beta \eta$$-conversion test for Martin-Löf type theory. Zbl 1157.68025
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
2008
On seminormality. Zbl 1102.13005
Coquand, Thierry
2006
Proof-theoretical analysis of order relations. Zbl 1062.03055
Negri, Sara; von Plato, Jan; Coquand, Thierry
2004
A presheaf model of parametric type theory. Zbl 1351.68146
Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem
2015
The projective spectrum as a distributive lattice. Zbl 1131.03035
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2007
Towards constructive homological algebra in type theory. Zbl 1202.68376
Coquand, Thierry; Spiwack, Arnaud
2007
Heitmann dimension of distributive lattices and commutative rings. Zbl 1158.13308
Coquand, Thierry; Lombardi, Henri; Quitté, Claude
2006
Geometric Hahn–Banach theorem. Zbl 1095.46046
Coquand, Thierry
2006
Compact spaces and distributive lattices. Zbl 1034.54005
Coquand, Thierry
2003
Sequents, frames, and completeness. Zbl 0973.03080
Coquand, Thierry; Zhang, Guo-Qiang
2000
Recursive functions and constructive mathematics. Zbl 1342.03043
Coquand, Thierry
2014
A computational interpretation of forcing in type theory. Zbl 1312.03021
Coquand, Thierry; Jaber, Guilhem
2012
Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768
Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David
2012
A nilregular element property. Zbl 1093.03035
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2005
On a theorem of Kronecker about algebraic varieties. Zbl 1039.13002
Coquand, Thierry
2004
Intuitionistic choice and classical logic. Zbl 0947.03078
Coquand, Thierry; Palmgren, Erik
2000
Gröbner bases in type theory. Zbl 0979.03044
1999
Two applications of Boolean models. Zbl 0904.03026
Coquand, Thierry
1998
An algorithm for type-checking dependent types. Zbl 0853.68102
Coquand, Thierry
1996
An analysis of Ramsey’s theorem. Zbl 0824.03034
Coquand, Thierry
1994
Une preuve directe du théorème d’ultime obstination. (A direct proof of the ultimate obstination theorem). Zbl 0749.68052
Coquand, Thierry
1992
A Kripke model for simplicial sets. Zbl 1350.18020
Bezem, Marc; Coquand, Thierry
2015
Games with 1-backtracking. Zbl 1241.03006
Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu
2010
A note on forcing and type theory. Zbl 1239.03041
Coquand, Thierry; Jaber, Guilhem
2010
Spectral schemes as ringed lattices. Zbl 1254.03114
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2009
On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
2008
A proof of strong normalisation using domain theory. Zbl 1131.68038
Coquand, Thierry; Spiwack, Arnaud
2007
A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301
Coquand, Thierry; Lombardi, Henri
2005
Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324
Bezem, Marc; Coquand, Thierry
2003
A finitary subsystem of the polymorphic $$\lambda$$-calculus. Zbl 0981.03020
Altenkirch, Thorsten; Coquand, Thierry
2001
The Hahn-Banach theorem in type theory. Zbl 0940.03069
Cederquist, Jan; Coquand, Thierry; Negri, Sara
1998
Minimal invariant spaces in formal topology. Zbl 0884.03058
Coquand, Thierry
1997
An application of constructive completeness. Zbl 1434.03098
Coquand, Thierry; Smith, Jan M.
1996
Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Zbl 0627.03045
Coquand, Thierry; Huet, Gérard
1987
The independence of Markov’s principle in type theory. Zbl 1434.03137
Coquand, Thierry; Mannaa, Bassel
2016
Non-constructivity in Kan simplicial sets. Zbl 1433.03154
Bezem, Marc; Coquand, Thierry; Parmann, Erik
2015
Isomorphism is equality. Zbl 1359.03010
Coquand, Thierry; Danielsson, Nils Anders
2013
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
2013
Coquand, Thierry
2013
Constructive finite free resolutions. Zbl 1239.13022
Coquand, Thierry; Quitté, Claude
2012
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
2011
Completeness theorems and $$\lambda$$-calculus. Zbl 1112.03307
Coquand, Thierry
2005
A logical framework with dependently typed records. Zbl 1095.03017
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto
2005
On the definition of reduction for infinite terms. Zbl 0859.68049
Coquand, Catarina; Coquand, Thierry
1996
A new paradox in type theory. Zbl 0821.03005
Coquand, Thierry
1994
Extensional models for polymorphism. Zbl 0636.03005
Breazu-Tannen, Val; Coquand, Thierry
1987
Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 07113696
Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan
2019
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
2017
Theory of dependent types and axiom of univalence. Zbl 1356.03002
Coquand, Thierry
2015
A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005
Barras, Bruno; Coquand, Thierry; Huber, Simon
2015
Revisiting Zariski main theorem from a constructive point of view. Zbl 1391.13049
Alonso, M. E.; Coquand, T.; Lombardi, H.
2014
Computing persistent homology within Coq/SSReflect. Zbl 1353.68251
Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2013
Coherent and strongly discrete rings in type theory. Zbl 1383.03016
Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2012
Metric complements of overt closed sets. Zbl 1251.03084
Coquand, Thierry; Palmgren, Erik; Spitters, Bas
2011
Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033
Barthe, Gilles; Coquand, Thierry
2006
Connecting a logical framework to a first-order logic prover. Zbl 1171.68712
Abel, Andreas; Coquand, Thierry; Norell, Ulf
2005
A logical framework with dependently typed records. Zbl 1052.68018
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto
2003
A representation of stably compact spaces, and patch topology. Zbl 1049.54027
Coquand, Thierry; Zhang, Guo-Qiang
2003
Metric Boolean algebras and constructive measure theory. Zbl 1064.03039
Coquand, Thierry; Palmgren, Erik
2002
A proof-theoretical investigation of Zantema’s problem. Zbl 0910.03033
1998
Computational content of classical logic. Zbl 0916.03035
Coquand, Thierry
1997
Inductive definitions and type theory. An introduction (preliminary version). Zbl 1044.03521
Coquand, Thierry; Dybjer, Peter
1994
Type theory and programming. Zbl 0791.68017
Coquand, Thierry; Nordström, Bengt; Smith, Jan M.; von Sydow, Björn
1994
On higher inductive types in cubical type theory. Zbl 1452.03036
Coquand, Thierry; Huber, Simon; Mörtberg, Anders
2018
Lattice-ordered groups generated by an ordered group and regular systems of ideals. Zbl 07113696
Coquand, Thierry; Lombardi, Henri; Neuwirth, Stefan
2019
Cubical type theory: a constructive interpretation of the univalence axiom. Zbl 1434.03036
Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders
2018
On higher inductive types in cubical type theory. Zbl 1452.03036
Coquand, Thierry; Huber, Simon; Mörtberg, Anders
2018
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
2017
The independence of Markov’s principle in type theory. Zbl 1434.03136
Coquand, Thierry; Mannaa, Bassel
2017
The independence of Markov’s principle in type theory. Zbl 1434.03137
Coquand, Thierry; Mannaa, Bassel
2016
A presheaf model of parametric type theory. Zbl 1351.68146
Bernardy, Jean-Philippe; Coquand, Thierry; Moulin, Guilhem
2015
A Kripke model for simplicial sets. Zbl 1350.18020
Bezem, Marc; Coquand, Thierry
2015
Non-constructivity in Kan simplicial sets. Zbl 1433.03154
Bezem, Marc; Coquand, Thierry; Parmann, Erik
2015
Theory of dependent types and axiom of univalence. Zbl 1356.03002
Coquand, Thierry
2015
A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005
Barras, Bruno; Coquand, Thierry; Huber, Simon
2015
A model of type theory in cubical sets. Zbl 1359.03009
Bezem, Marc; Coquand, Thierry; Huber, Simon
2014
Recursive functions and constructive mathematics. Zbl 1342.03043
Coquand, Thierry
2014
Revisiting Zariski main theorem from a constructive point of view. Zbl 1391.13049
Alonso, M. E.; Coquand, T.; Lombardi, H.
2014
Isomorphism is equality. Zbl 1359.03010
Coquand, Thierry; Danielsson, Nils Anders
2013
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
2013
Coquand, Thierry
2013
Computing persistent homology within Coq/SSReflect. Zbl 1353.68251
Heras, Jónathan; Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2013
Dynamic Newton-Puiseux theorem. Zbl 1345.03115
Mannaa, Bassel; Coquand, Thierry
2013
A computational interpretation of forcing in type theory. Zbl 1312.03021
Coquand, Thierry; Jaber, Guilhem
2012
Stop when you are almost-full. Adventures in constructive termination. Zbl 1360.68768
Vytiniotis, Dimitrios; Coquand, Thierry; Wahlstedt, David
2012
Constructive finite free resolutions. Zbl 1239.13022
Coquand, Thierry; Quitté, Claude
2012
Coherent and strongly discrete rings in type theory. Zbl 1383.03016
Coquand, Thierry; Mörtberg, Anders; Siles, Vincent
2012
A decision procedure for regular expression equivalence in type theory. Zbl 1350.68228
Coquand, Thierry; Siles, Vincent
2011
A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Zbl 1213.68199
Abel, Andreas; Coquand, Thierry; Pagano, Miguel
2011
Metric complements of overt closed sets. Zbl 1251.03084
Coquand, Thierry; Palmgren, Erik; Spitters, Bas
2011
Unique paths as formal points. Zbl 1296.03036
Coquand, Thierry; Schuster, Peter
2011
Games with 1-backtracking. Zbl 1241.03006
Berardi, Stefano; Coquand, Thierry; Hayashi, Susumu
2010
A note on forcing and type theory. Zbl 1239.03041
Coquand, Thierry; Jaber, Guilhem
2010
Constructive theory of Banach algebras. Zbl 1285.03073
Coquand, Thierry; Spitters, Bas
2010
Constructively finite? Zbl 1217.03046
Coquand, Thierry; Spiwack, Arnaud
2010
Space of valuations. Zbl 1222.03072
Coquand, Thierry
2009
Integrals and valuations. Zbl 1245.03098
Coquand, Thierry; Spitters, Bas
2009
Constructive Gelfand duality for C$$^*$$-algebras. Zbl 1183.46052
Coquand, Thierry; Spitters, Bas
2009
Constructive Krull dimension. I: Integral extensions. Zbl 1172.13007
Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitté, Claude
2009
Spectral schemes as ringed lattices. Zbl 1254.03114
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2009
A simple type-theoretic language: Mini-TT. Zbl 1184.68152
Coquand, Thierry; Kinoshita, Yoshiki; Nordström, Bengt; Takeyama, Makoto
2009
Verifying a semantic $$\beta \eta$$-conversion test for Martin-Löf type theory. Zbl 1157.68025
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
2008
On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570
Abel, Andreas; Coquand, Thierry; Dybjer, Peter
2008
A note on the axiomatisation of real numbers. Zbl 1172.03030
Coquand, Thierry; Lombardi, L. Henri
2008
The projective spectrum as a distributive lattice. Zbl 1131.03035
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2007
Towards constructive homological algebra in type theory. Zbl 1202.68376
Coquand, Thierry; Spiwack, Arnaud
2007
A proof of strong normalisation using domain theory. Zbl 1131.68038
Coquand, Thierry; Spiwack, Arnaud
2007
Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Zbl 1121.68026
Abel, Andreas; Coquand, Thierry
2007
A logical approach to abstract algebra. Zbl 1118.03059
Coquand, Thierry; Lombardi, Henri
2006
On seminormality. Zbl 1102.13005
Coquand, Thierry
2006
Heitmann dimension of distributive lattices and commutative rings. Zbl 1158.13308
Coquand, Thierry; Lombardi, Henri; Quitté, Claude
2006
Geometric Hahn–Banach theorem. Zbl 1095.46046
Coquand, Thierry
2006
Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033
Barthe, Gilles; Coquand, Thierry
2006
Formalising bitonic sort in type theory. Zbl 1172.68439
Bove, Ana; Coquand, Thierry
2006
About Stone’s notion of spectrum. Zbl 1061.06031
Coquand, Thierry
2005
Automating coherent logic. Zbl 1143.03332
Bezem, Marc; Coquand, Thierry
2005
An elementary characterization of Krull dimension. Zbl 1161.54303
Coquand, Thierry; Lombardi, Henri; Roy, Marie-Françoise
2005
Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049
Coquand, T.; Spitters, B.
2005
A nilregular element property. Zbl 1093.03035
Coquand, Thierry; Lombardi, Henri; Schuster, Peter
2005
A short proof for the Krull dimension of a polynomial ring. Zbl 1105.13301
Coquand, Thierry; Lombardi, Henri
2005
Completeness theorems and $$\lambda$$-calculus. Zbl 1112.03307
Coquand, Thierry
2005
A logical framework with dependently typed records. Zbl 1095.03017
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto
2005
Connecting a logical framework to a first-order logic prover. Zbl 1171.68712
Abel, Andreas; Coquand, Thierry; Norell, Ulf
2005
A completeness proof for geometrical logic. Zbl 1101.03026
Coquand, Thierry
2005
Generating non-Noetherian modules constructively. Zbl 1059.13006
Coquand, Thierry; Lombardi, Henri; Quitté, Claude
2004
Proof-theoretical analysis of order relations. Zbl 1062.03055
Negri, Sara; von Plato, Jan; Coquand, Thierry
2004
On a theorem of Kronecker about algebraic varieties. Zbl 1039.13002
Coquand, Thierry
2004
Newman’s lemma – a case study in proof automation and geometric logic. Zbl 1063.68089
Bezem, Marc; Coquand, Thierry
2004
Inductively generated formal topologies. Zbl 1070.03041
Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio
2003
Hidden constructions in abstract algebra: Krull dimension of distributive lattice and commutative rings. Zbl 1096.13507
Coquand, Thierry; Lombardi, Henri
2003
Compact spaces and distributive lattices. Zbl 1034.54005
Coquand, Thierry
2003
Newman’s Lemma – a case study in proof automation and geometric logic. Zbl 1169.03324
Bezem, Marc; Coquand, Thierry
2003
A logical framework with dependently typed records. Zbl 1052.68018
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto
2003
A representation of stably compact spaces, and patch topology. Zbl 1049.54027
Coquand, Thierry; Zhang, Guo-Qiang
2003
A syntactical proof of the Marriage Lemma. Zbl 1051.03048
Coquand, Thierry
2003
Metric Boolean algebras and constructive measure theory. Zbl 1064.03039
Coquand, Thierry; Palmgren, Erik
2002
An introduction to dependent type theory. Zbl 1065.68025
Barthe, Gilles; Coquand, Thierry
2002
An implementation of Type:Type. Zbl 1054.68087
Coquand, Thierry; Takeyama, Makoto
2002
Valuations and Dedekind’s Prague theorem. Zbl 0983.11061
2001
A finitary subsystem of the polymorphic $$\lambda$$-calculus. Zbl 0981.03020
Altenkirch, Thorsten; Coquand, Thierry
2001
Entailment relations and distributive lattices. Zbl 0948.03056
Cederquist, Jan; Coquand, Thierry
2000
Formal topologies on the set of first-order formulae. Zbl 0965.03072
Coquand, Thierry; Sadocco, Sara; Sambin, Giovanni; Smith, Jan M.
2000
Sequents, frames, and completeness. Zbl 0973.03080
Coquand, Thierry; Zhang, Guo-Qiang
2000
Intuitionistic choice and classical logic. Zbl 0947.03078
Coquand, Thierry; Palmgren, Erik
2000
A new method for establishing conservativity of classical systems over their intuitionistic version. Zbl 0935.03069
Coquand, Thierry; Hofmann, Martin
1999
Gröbner bases in type theory. Zbl 0979.03044
1999
A Boolean model of ultrafilters. Zbl 0930.03042
Coquand, Thierry
1999
On the computational content of the axiom of choice. Zbl 0914.03059
Berardi, Stefano; Bezem, Marc; Coquand, Thierry
1998
Two applications of Boolean models. Zbl 0904.03026
Coquand, Thierry
1998
The Hahn-Banach theorem in type theory. Zbl 0940.03069
Cederquist, Jan; Coquand, Thierry; Negri, Sara
1998
A proof-theoretical investigation of Zantema’s problem. Zbl 0910.03033
1998
A note on formal iterated function systems. Zbl 0958.68149
Coquand, Thierry
1998
Intuitionistic model constructions and normalization proofs. Zbl 0883.03009
Coquand, Thierry; Dybjer, Peter
1997
Minimal invariant spaces in formal topology. Zbl 0884.03058
Coquand, Thierry
1997
Computational content of classical logic. Zbl 0916.03035
Coquand, Thierry
1997
An algorithm for type-checking dependent types. Zbl 0853.68102
Coquand, Thierry
1996
An application of constructive completeness. Zbl 1434.03098
Coquand, Thierry; Smith, Jan M.
1996
On the definition of reduction for infinite terms. Zbl 0859.68049
Coquand, Catarina; Coquand, Thierry
1996
A semantics of evidence for classical arithmetic. Zbl 0829.03037
Coquand, Thierry
1995
A constructive topological proof of van der Waerden’s theorem. Zbl 0841.03032
Coquand, Thierry
1995
$$A$$-translation and looping combinators in pure type systems. Zbl 0817.03007
Coquand, Thierry; Herbelin, Hugo
1994
An analysis of Ramsey’s theorem. Zbl 0824.03034
Coquand, Thierry
1994
A new paradox in type theory. Zbl 0821.03005
Coquand, Thierry
1994
Inductive definitions and type theory. An introduction (preliminary version). Zbl 1044.03521
Coquand, Thierry; Dybjer, Peter
1994
...and 20 more Documents
all top 5

#### Cited by 659 Authors

 38 Coquand, Thierry 23 Lombardi, Henri 13 Spitters, Bas 12 Dybjer, Peter 12 Schuster, Peter Michael 12 Yengui, Ihsen 11 Berardi, Stefano 10 Valentini, Silvio 9 Rinaldi, Davide 9 Sambin, Giovanni 8 Hötzel Escardó, Martín 8 Luo, Zhaohui 7 Abel, Andreas M. 7 Ciraulo, Francesco 7 Ducos, Lionel 7 Vickers, Steven 7 Wessel, Daniel 6 Aschieri, Federico 6 Avigad, Jeremy 6 Berger, Ulrich 6 Curi, Giovanni 6 Dufourd, Jean-François 6 Oliva, Paulo 6 Quitté, Claude 6 Rubio García, Julio Jesús 5 Altenkirch, Thorsten 5 Barbanera, Franco 5 Bezem, Marc 5 Bove, Ana 5 Dyckhoff, Roy 5 Ghani, Neil 5 Harper, Robert 5 Kamareddine, Fairouz D. 5 Kawai, Tatsuji 5 Palmgren, Erik 5 Pfenning, Frank 5 Pitts, Andrew M. 5 Rabe, Florian 4 Abramsky, Samson 4 Barthe, Gilles 4 Curien, Pierre-Louis 4 de’Liguoro, Ugo 4 Duggan, Dominic 4 Farmer, William M. 4 Heunen, Chris 4 Honsell, Furio 4 Janičić, Predrag 4 Jung, Achim 4 Landsman, Nicolaas P. 4 Møgelberg, Rasmus Ejlers 4 Negri, Sara 4 Nordvall Forsberg, Fredrik 4 Powell, Thomas M. 4 Seldin, Jonathan P. 4 Wadler, Philip Lee 3 Ahrens, Benedikt 3 Akama, Yohji 3 Alonso García, María Emilia 3 Aransay, Jesús 3 Asperti, Andrea 3 Awodey, Steve 3 Barhoumi, Sami 3 Blanqui, Frédéric 3 Breazu-Tannen, Val 3 Bruce, Kim B. 3 Buchholtz, Ulrik 3 Compagnoni, Adriana B. 3 Dehlinger, Christophe 3 Felty, Amy P. 3 Fu, Yuxi 3 Gallier, Jean H. 3 Gambino, Nicola 3 Hatcliff, John 3 Hendriks, Dimitri 3 Henry, Simon 3 Huber, Simon 3 Ishihara, Hajime 3 Jacobs, Bart 3 Komendantskaya, Ekaterina 3 Maietti, Maria Emilia 3 Moerdijk, Ieke 3 Moshier, M. Andrew 3 Nadathur, Gopalan 3 Nederpelt, Rob 3 Orsanigo, Federico 3 Orton, Ian 3 Polonsky, Andrew 3 Ruiz-Reina, José-Luis 3 Schrijvers, Tom 3 Schürmann, Carsten 3 Schwichtenberg, Helmut 3 Scott, Philip J. 3 Shulman, Michael A. 3 Smolka, Gert 3 Sørensen, Morten Heine B. 3 Steila, Silvia 3 Streicher, Thomas 3 Szasz, Nora 3 Tasistro, Alvaro 3 Tassi, Enrico ...and 559 more Authors
all top 5

#### Cited in 92 Serials

 93 Theoretical Computer Science 73 Annals of Pure and Applied Logic 37 Information and Computation 37 MSCS. Mathematical Structures in Computer Science 26 Journal of Automated Reasoning 19 Journal of Algebra 19 The Journal of Symbolic Logic 18 Logical Methods in Computer Science 17 Journal of Functional Programming 15 Journal of Symbolic Computation 12 Journal of Pure and Applied Algebra 12 Archive for Mathematical Logic 11 Formal Aspects of Computing 7 Studia Logica 7 The Bulletin of Symbolic Logic 6 Annals of Mathematics and Artificial Intelligence 5 Synthese 5 Mathematical Logic Quarterly (MLQ) 5 The Journal of Logic and Algebraic Programming 4 Indagationes Mathematicae. New Series 4 Journal of Applied Logic 3 Acta Informatica 3 Communications in Algebra 3 Journal of Philosophical Logic 3 Journal of Computer Science and Technology 3 Theory of Computing Systems 3 RAIRO. Theoretical Informatics and Applications 3 Foundations of Physics 3 Journal of Logical and Algebraic Methods in Programming 3 Higher Structures 2 Computers & Mathematics with Applications 2 Communications in Mathematical Physics 2 Mathematical Proceedings of the Cambridge Philosophical Society 2 Archiv der Mathematik 2 Mathematische Zeitschrift 2 Notre Dame Journal of Formal Logic 2 Proceedings of the American Mathematical Society 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 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 Journal of Logic and Analysis 1 Information Processing Letters 1 Journal of Mathematical Physics 1 Mathematics of Computation 1 The Mathematical Intelligencer 1 Advances in Mathematics 1 Algebra Universalis 1 Collectanea Mathematica 1 Dissertationes Mathematicae 1 Fuzzy Sets and Systems 1 Information Sciences 1 Linguistics and Philosophy 1 Manuscripta Mathematica 1 Mathematische Nachrichten 1 Mathematica Scandinavica 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 Applied Categorical Structures 1 Journal of Applied Non-Classical Logics 1 Advances in Applied Clifford Algebras 1 The New York Journal of Mathematics 1 Theory and Applications of Categories 1 Topoi 1 Higher-Order and Symbolic Computation 1 Journal of the Australian Mathematical Society 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 Journal of Algebra and its Applications 1 Electronic Notes in Theoretical Computer Science 1 Logica Universalis 1 Confluentes Mathematici 1 Journal of Commutative Algebra 1 São Paulo Journal of Mathematical Sciences 1 The Review of Symbolic Logic 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Actes des Rencontres du C.I.R.M.
all top 5

#### Cited in 37 Fields

 419 Mathematical logic and foundations (03-XX) 366 Computer science (68-XX) 76 Category theory; homological algebra (18-XX) 67 Order, lattices, ordered algebraic structures (06-XX) 57 Commutative algebra (13-XX) 39 General topology (54-XX) 20 Algebraic topology (55-XX) 19 Algebraic geometry (14-XX) 12 Functional analysis (46-XX) 9 Combinatorics (05-XX) 9 $$K$$-theory (19-XX) 9 Quantum theory (81-XX) 9 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 8 Associative rings and algebras (16-XX) 6 History and biography (01-XX) 6 General algebraic systems (08-XX) 4 General and overarching topics; collections (00-XX) 4 Field theory and polynomials (12-XX) 4 Operator theory (47-XX) 4 Numerical analysis (65-XX) 3 Measure and integration (28-XX) 2 Number theory (11-XX) 2 Group theory and generalizations (20-XX) 2 Real functions (26-XX) 2 Partial differential equations (35-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Convex and discrete geometry (52-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Nonassociative rings and algebras (17-XX) 1 Several complex variables and analytic spaces (32-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 Biology and other natural sciences (92-XX) 1 Systems theory; control (93-XX)

#### Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.