×

zbMATH — the first resource for mathematics

Coquand, Thierry

Compute Distance To:
Author ID: coquand.thierry Recent zbMATH articles by "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

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

Publications by Year

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

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.