Thierry Coquand
#6,404
Most Influential Person Now
French mathematician, logician and computer scientist
Thierry Coquand's AcademicInfluence.com Rankings
Thierry Coquandphilosophy Degrees
Philosophy
#1247
World Rank
#2305
Historical Rank
Logic
#212
World Rank
#457
Historical Rank
Download Badge
Computer Science Philosophy
Thierry Coquand's Degrees
- PhD Mathematics Université Paris Cité
Why Is Thierry Coquand Influential?
(Suggest an Edit or Addition)According to Wikipedia, Thierry Coquand is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg, having previously worked at INRIA. He is known for his work in constructive mathematics, especially the calculus of constructions.
Thierry Coquand's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- The Calculus of Constructions (1988) (1345)
- Inductively defined types (1988) (360)
- Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom (2015) (293)
- Constructions: A Higher Order Proof System for Mechanizing Mathematics (1985) (249)
- An Analysis of Girard's Paradox (1986) (222)
- A Model of Type Theory in Cubical Sets (2013) (216)
- Inheritance as Implicit Coercion (1991) (203)
- Pattern Matching with Dependent Types (1992) (186)
- An algorithm for testing conversion in type theory (1991) (151)
- A semantics of evidence for classical arithmetic (1995) (147)
- Metamathematical investigations of a calculus of constructions (1989) (142)
- Inductively generated formal topologies (2003) (139)
- On seminormality (2006) (124)
- On the computational content of the axiom of choice (1994) (115)
- An Algorithm for Type-Checking Dependent Types (1996) (95)
- Domain Theoretic Models of Polymorphism (1989) (94)
- Krull Dimension (2000) (91)
- Infinite Objects in Type Theory (1994) (89)
- Intuitionistic model constructions and normalization proofs (1997) (85)
- Inheritance and explicit coercion (1989) (78)
- Entailment relations and distributive lattices (2000) (71)
- Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings (2017) (69)
- On Higher Inductive Types in Cubical Type Theory (2018) (68)
- Extensional Models for Polymorphism (1987) (64)
- A Logical Framework with Dependently Typed Records (2003) (61)
- DI-Domains as a Model of Polymorphism (1987) (60)
- Generating non-Noetherian modules constructively (2004) (55)
- Integrals and valuations (2008) (51)
- Automating Coherent Logic (2005) (49)
- A Presheaf Model of Parametric Type Theory (2015) (48)
- A logical approach to abstract algebra (2005) (46)
- A new method for establishing conservativity of classical systems over their intuitionistic version (1999) (46)
- A-translation and looping combinators in pure type systems (1994) (44)
- Categories of embeddings (1988) (44)
- Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (2007) (43)
- A Proof of Strong Normalization for the Theor y of Constructions Using a Kripke-like Interpretation (1990) (40)
- About Stone's notion of spectrum (2005) (40)
- Constructive Topology and Combinatorics (1992) (39)
- A Decision Procedure for Regular Expression Equivalence in Type Theory (2011) (37)
- Canonicity and normalisation for Dependent Type Theory (2018) (35)
- Notions of Anonymous Existence in Martin-Löf Type Theory (2016) (35)
- An elementary characterization of Krull dimension (2005) (34)
- Constructive Gelfand duality for C*-algebras (2008) (34)
- A Proof of Strong Normalisation using Domain Theory (2006) (31)
- The Independence of Markov's Principle in Type Theory (2016) (31)
- Proof-theoretical analysis of order relations (2004) (30)
- Sequents, Frames, and Completeness (2000) (30)
- Stop When You Are Almost-Full - Adventures in Constructive Termination (2012) (30)
- Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems (2008) (29)
- Syntax and models of Cartesian cubical type theory (2021) (29)
- Valuations and Dedekind's Prague Theorem (2001) (29)
- A new paradox in type theory (1995) (29)
- Space of valuations (2009) (28)
- The Hahn-Banach Theorem in Type Theory (1998) (27)
- Isomorphism is equality (2013) (26)
- An intuitionistic proof of Tychonoff's theorem (1992) (26)
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (2008) (26)
- The Univalence Axiom in Cubical Sets (2017) (26)
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (2009) (25)
- Stack semantics of type theory (2017) (25)
- Homotopy Type Theory: Univalent Foundations of Mathematics (2013) (23)
- Towards Constructive Homological Algebra in Type Theory (2007) (23)
- Homotopy canonicity for cubical type theory (2019) (22)
- Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column (2003) (22)
- A proof of Higman's lemma by structural induction (1993) (22)
- An Equational Presentation of Higher Order Logic (1987) (22)
- A Kripke model for simplicial sets (2015) (21)
- Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs (2007) (20)
- The projective spectrum as a distributive lattice (2007) (20)
- A generalization of the Takeuti–Gandy interpretation (2015) (20)
- Gröbner Bases in Type Theory (1998) (20)
- Computing persistent homology within Coq/SSReflect (2012) (19)
- Computational Content of Classical Logic (1996) (19)
- Intuitionistic choice and classical logic (2000) (19)
- Generalizations of Hedberg's Theorem (2013) (19)
- A Cubical Type Theory (2015) (18)
- Formal topologies on the set of first-order formulae (2000) (18)
- Cartesian Cubical Type Theory (2017) (18)
- Metric Boolean algebras and constructive measure theory (2002) (18)
- Lattice-ordered groups generated by an ordered group and regular systems of ideals (2017) (18)
- A nilregular element property (2005) (18)
- A Note on the Open Induction Principle (1997) (17)
- On the analogy between propositions and types (1986) (17)
- A Note on Forcing and Type Theory (2010) (16)
- Inductive Definitions and Type Theory: an Introduction (Preliminary Version) (1994) (16)
- A Computational Interpretation of Forcing in Type Theory (2012) (16)
- Spectral schemes as ringed lattices (2009) (16)
- Constructive Krull Dimension. I: Integral Extensions (2009) (16)
- Non-Constructivity in Kan Simplicial Sets (2015) (15)
- Connecting a Logical Framework to a First-Order Logic Prover (2005) (14)
- Compact spaces and distributive lattices (2003) (14)
- INHERITANCE AND EXPLICIT COERCION (Preliminary Report) (1989) (14)
- A Short Proof for the Krull Dimension of a Polynomial Ring (2005) (14)
- An Analysis of Ramsey's Theorem (1994) (13)
- Editors' note: bibliometrics and the curators of orthodoxy (2009) (13)
- Dynamic Newton-Puiseux theorem (2013) (13)
- An Application of Constructive Completeness (1995) (12)
- Geometric Hahn-Banach theorem (2006) (12)
- An elementary characterisation of Krull dimension (2005) (12)
- Completeness Theorems and lambda-Calculus (2005) (11)
- An Introduction to Dependent Type Theory (2000) (11)
- Recursive Functions and Constructive Mathematics (2014) (11)
- An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951) (2017) (11)
- Games with 1-backtracking (2010) (11)
- Constructive finite free resolutions (2012) (11)
- The paradox of trees in type theory (1992) (10)
- A representation of stably compact spaces, and patch topology (2003) (10)
- Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory (2008) (10)
- A simple type-theoretic language: Mini-TT (2009) (10)
- About Brouwer's fan theorem (2004) (10)
- A formal proof of Sasaki-Murao algorithm (2012) (9)
- A Completeness Proof for Geometrical Logic (2005) (9)
- A Finitary Subsystem of the Polymorphic lambda-Calculus (2001) (8)
- Two applications of Boolean models (1998) (8)
- The Wiener lemma and certain of its generalizations (1991) (8)
- Minimal invariant spaces in formal topology (1997) (8)
- Coherent and Strongly Discrete Rings in Type Theory (2012) (8)
- Type Theory and Programming (2007) (8)
- Constructive sheaf models of type theory (2019) (8)
- Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality (2019) (8)
- Dependent type theory as the initial category with families (2014) (7)
- Formalising Bitonic Sort in Type Theory (2004) (7)
- Constructive theory of Banach algebras (2010) (7)
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (2008) (7)
- Kolmogorov’s contribution to intuitionistic logic (2007) (7)
- A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction (1985) (6)
- Curves and coherent Prüfer rings (2010) (6)
- A constructive version of Laplace's proof on the existence of complex roots (2013) (6)
- Remarks on the equational theory of non-normalizing pure type systems (2003) (6)
- A Proof-Theoretical Investigation of Zantema's Problem (1997) (5)
- Unique paths as formal points (2011) (5)
- In nite Objects in Type Theory (2007) (5)
- A constructive proof of the Peter‐Weyl theorem (2005) (5)
- About Goodman's Theorem (2013) (5)
- An Implementation of Type: Type (2000) (5)
- Type Theorie Programming (1994) (5)
- Philosophy and Foundations of Mathematics: Epistemological and Ontological Aspects (2009) (5)
- A constructive topological proof of van der Waerden's theorem (1995) (5)
- Metric complements of overt closed sets (2009) (5)
- A note on measures with values in a partially ordered vector space (2004) (4)
- Lorenzen's Proof of Consistency for Elementary Number Theory (2020) (4)
- On a theorem of Kronecker about algebraic sets (2004) (4)
- Semantics and Logics of Computation: Computational Content of Classical Logic Thierry Coquand (1997) (4)
- Canonicity and homotopy canonicity for cubical type theory (2019) (4)
- Grr Obner Bases in Type Theory (1998) (4)
- A Sheaf Model of the Algebraic Closure (2014) (4)
- Formal Topology with Posets (1996) (4)
- A syntactical proof of the Marriage Lemma (2003) (3)
- Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism (2022) (3)
- A note on the axiomatisation of real numbers (2008) (3)
- Constructive theory of ordinals (2022) (3)
- Modules as Dependently Typed Records (2002) (3)
- Reduction Free Normalisation for a proof irrelevant type of propositions (2021) (3)
- Constructive mathematics and functional programming (2008) (3)
- A survey of constructive presheaf models of univalence (2018) (3)
- A realization of the negative interpretation of the Axiom of Choice (1995) (3)
- Negative consistent axioms can be postulated without loss of canonicity (2013) (3)
- A constructive proof of Gelfand duality for C*-algebras (2008) (2)
- Constructive Mathematics and Functional Programming (Abstract) (2008) (2)
- Program Construction in Intuitionistic Type Theory (Abstract) (1995) (2)
- Some Remarks about Normal Rings (2022) (2)
- Alfa/Agda (2006) (2)
- Another Proof of the Intuitionistic Ramsey Theorem (1993) (2)
- Forcing and Type Theory (2009) (2)
- Completeness Theorems and λ-Calculus (2005) (2)
- Regular Entailment Relations (2019) (2)
- On the Equational Theory of Non-Normalising Pure Type Systems (2001) (2)
- Dimension de Krull explicite. Application aux théorèmes de Kronecker, Bass, Serre et Foster (2004) (1)
- 05021 Abstracts Collection -- Mathematics, Algorithms, Proofs (2005) (1)
- Formal Topology and Univalent Foundations (2021) (1)
- Mini-Workshop: Formal Methods in Commutative Algebra: A View Toward Constructive Homological Algebra (2009) (1)
- The Ackermann Award 2012 (2012) (1)
- Constructive basic theory of central simple algebras (2021) (1)
- A constructive proof of Simpson's Rule (2012) (1)
- Inheritance as Implicit Coercion 1 (1991) (1)
- Constructions cach\'ees en alg\`ebre abstraite (3) Dimension de Krull, Going Up, Going Down (2017) (1)
- Computable sets : located and overt locales (2007) (1)
- Lorenzen and Constructive Mathematics (2021) (1)
- Type Theories with Universe Level Judgements (2022) (1)
- A Direct Proof of the Intuitionistic Ramsey Theorem (1991) (1)
- An elementary proof of Wiebe's Theorem (2018) (1)
- A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic (2016) (1)
- Revisiting Zariski Main Theorem from a constructive point of view (2014) (1)
- Types for Proofs and Programs (2002) (1)
- Types for Proofs and Programs - nternational Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers (Lecture Notes in Computer Science, Vol. 1956) (2000) (1)
- Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down (2017) (1)
- Skolem's Theorem in Coherent Logic (2019) (1)
- Types for proofs and programs : International Workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers (2000) (1)
- An Adequacy Theorem for Dependent Type Theory (2018) (1)
- Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472) (2021) (1)
- A Boolean Model of Ultrafilters (1999) (1)
- Dynamical Method in Algebra: A Survey (2003) (0)
- Constructive finite free resolutions (2011) (0)
- Transfinite Games - To the infinite and beyond! (1998) (0)
- The Completeness of Typing for Context-Semantics (2007) (0)
- Preface to the special issue for The Fifth Workshop on Formal Topology (2019) (0)
- General Presentation 05021 Summary -mathematics, Algorithms, Proofs (0)
- Mathematics, Algorithms, Proofs, 9.-14. January 2005 (2006) (0)
- Proof Theory in Type Theory (1996) (0)
- MSC volume 23 issue 5 Cover and Back matter (2013) (0)
- Algebraically Closed Fields (2019) (0)
- A Sheaf Model of the Algebraic Closure Bassel Mannaa (2014) (0)
- The Univalence Axiom in Cubical Sets (2018) (0)
- Algebraic Closure (2000) (0)
- Combinatorial topology and constructive mathematics (2018) (0)
- A Boolean Model of Ultraalters (0)
- Type Theory and Univalent Foundation (2013) (0)
- Preface (2006) (0)
- Preface to the French Edition (2019) (0)
- Inductive Deenitions and Type Theory an Introduction 1.1 Prehistory 1.1.1 Induction on the Natural Numbers (1994) (0)
- L O ] 2 M ay 2 02 3 Type Theory with Explicit Universe Polymorphism (2023) (0)
- forcing in type theory (2009) (0)
- R\'esolutions libres finies. M\'ethodes constructives (2018) (0)
- 05021 Executive Summary -- Mathematics, Algorithms, Proofs (2005) (0)
- MSC volume 21 issue 5 Cover and Back matter (2011) (0)
- A Note on Formal Iterated Function Systems (2000) (0)
- Verification and Constructive Algebra (Dagstuhl Seminar 03021) (2021) (0)
- MSC volume 22 issue 4 Cover and Back matter (2012) (0)
- Type Theory and Formalisation of Mathematics (2017) (0)
- The Ackermann Award 2016 (2016) (0)
- Mini-Workshop: Constructive Homological Algebra with Applications to Coherent Sheaves and Control Theory (2013) (0)
- Syntactic forcing models for coherent logic (2017) (0)
- On generalized algebraic theories and categories with families (2020) (0)
- 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia (2018) (0)
- Selected papers from the International Workshop on Types for Proofs and Programs (1994) (0)
- Preface (2016) (0)
- Inner Models of Univalence (2018) (0)
- Realizability at Work: Separating Two Constructive Notions of Finiteness (2018) (0)
- FORMAL TOPOLOGY AND CONSTRUCTIVE MATHEMATICS (2008) (0)
- Prague, Czech Republic, August 9–15, 1998 (1999) (0)
- Preface of special issue on formal topology (2006) (0)
- Infinite objects in constructive mathematics (2005) (0)
- Veri cation and Constructive Algebra (2004) (0)
- Inductive Solution of Borel's Measure Problem (1999) (0)
- Course Notes in Typed Lambda Calculus (1998) (0)
- A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic (2016) (0)
- Preface (2012) (0)
- The Real Spectrum (2019) (0)
- An Adequacy Theorem for Dependent Type Theory (2018) (0)
- Kearnes, KA, Kiss, EW and Valeriote, MA, A geometric (1999) (0)
- Controlling unfolding in type theory (2022) (0)
- 05021 Abstracts Collection Mathematics , Algorithms , Proofs Dagstuhl Seminar (2006) (0)
- A Topological Model of Ultraalters (1997) (0)
This paper list is powered by the following services:
Other Resources About Thierry Coquand
What Schools Are Affiliated With Thierry Coquand?
Thierry Coquand is affiliated with the following schools:
