Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Thierry Coquand
2010 – today
- 2013
[j49]- [c49]Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch: Generalizations of Hedberg's Theorem. TLCA 2013: 173-188
- 2012
- [j48]Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster: Preface. Ann. Pure Appl. Logic 163(2): 85-86 (2012)
- [c48]Thierry Coquand, Anders Mörtberg, Vincent Siles: Coherent and Strongly Discrete Rings in Type Theory. CPP 2012: 273-288
- [c47]
- [c46]Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt: Stop When You Are Almost-Full - Adventures in Constructive Termination. ITP 2012: 250-265
- [p1]Thierry Coquand, Guilhem Jaber: A Computational Interpretation of Forcing in Type Theory. Epistemology versus Ontology 2012: 203-213
- [i2]Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles: Computing Persistent Homology within Coq/SSReflect. CoRR abs/1209.1905 (2012)
- 2011
- [j47]Andreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance. Logical Methods in Computer Science 7(2) (2011)
- [j46]Thierry Coquand, Erik Palmgren, Bas Spitters: Metric complements of overt closed sets. Math. Log. Q. 57(4): 373-378 (2011)
- [c45]Thierry Coquand, Vincent Siles: A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP 2011: 119-134
- 2010
- [j45]Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. Ann. Pure Appl. Logic 161(10): 1254-1269 (2010)
- [j44]Thierry Coquand, Guilhem Jaber: A Note on Forcing and Type Theory. Fundam. Inform. 100(1-4): 43-52 (2010)
- [j43]Thierry Coquand, Henri Lombardi, Claude Quitté: Curves and coherent Prüfer rings. J. Symb. Comput. 45(12): 1378-1390 (2010)
2000 – 2009
- 2009
- [j42]Thierry Coquand, Henri Lombardi, Peter Schuster: Spectral schemes as ringed lattices. Ann. Math. Artif. Intell. 56(3-4): 339-360 (2009)
- [j41]
- [c44]
- [c43]Andreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009: 5-19
- 2008
- [j40]Thierry Coquand, Henri Lombardi: A note on the axiomatisation of real numbers. Math. Log. Q. 54(3): 224-228 (2008)
- [c42]
- [c41]Andreas Abel, Thierry Coquand, Peter Dybjer: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13
- [c40]Andreas Abel, Thierry Coquand, Peter Dybjer: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56
- 2007
- [j39]Thierry Coquand: The Completeness of Typing for Context-Semantics. Fundam. Inform. 77(4): 293-301 (2007)
- [j38]Andreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Inform. 77(4): 345-395 (2007)
- [j37]Thierry Coquand, Arnaud Spiwack: A proof of strong normalisation using domain theory. Logical Methods in Computer Science 3(4) (2007)
- [c39]Andreas Abel, Thierry Coquand, Peter Dybjer: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12
- [c38]Thierry Coquand, Arnaud Spiwack: Towards Constructive Homological Algebra in Type Theory. Calculemus/MKM 2007: 40-54
- [i1]Thierry Coquand, Arnaud Spiwack: A proof of strong normalisation using domain theory. CoRR abs/0709.1401 (2007)
- 2006
- [j36]Bernhard Banaschewski, Thierry Coquand, Giovanni Sambin: Preface. Ann. Pure Appl. Logic 137(1-3): 1-2 (2006)
- [j35]Gilles Barthe, Thierry Coquand: Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16(2): 137-155 (2006)
- [j34]Thierry Coquand, Henri Lombardi: A logical approach to abstract algebra. Mathematical Structures in Computer Science 16(5): 885-900 (2006)
- [c37]Thierry Coquand, Arnaud Spiwack: A Proof of Strong Normalisation using Domain Theory. LICS 2006: 307-316
- [c36]
- [e2]Thierry Coquand, Henri Lombardi, Marie-Françoise Roy (Eds.): Mathematics, Algorithms, Proofs, 9.-14. January 2005. Dagstuhl Seminar Proceedings 05021, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006
- 2005
- [j33]Thierry Coquand, Randy Pollack, Makoto Takeyama: A Logical Framework with Dependently Typed Records. Fundam. Inform. 65(1-2): 113-134 (2005)
- [j32]Thierry Coquand, Bas Spitters: Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. UCS 11(12): 1932-1944 (2005)
- [j31]Thierry Coquand, Bas Spitters: A constructive proof of the Peter-Weyl theorem. Math. Log. Q. 51(4): 351-359 (2005)
- [j30]Thierry Coquand, Henri Lombardi: A Short Proof for the Krull Dimension of a Polynomial Ring. The American Mathematical Monthly 112(9): 826-829 (2005)
- [c35]
- [c34]Thierry Coquand: 05021 Executive Summary -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005
- [c33]Thierry Coquand, Henri Lombardi, Marie-Françoise Roy: 05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005
- [c32]Thierry Coquand, Henri Lombardi, Peter Schuster: A Nilregular Element Property. Mathematics, Algorithms, Proofs 2005
- [c31]Andreas Abel, Thierry Coquand, Ulf Norell: Connecting a Logical Framework to a First-Order Logic Prover. FroCoS 2005: 285-301
- [c30]
- [c29]
- [c28]
- [c27]Andreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA 2005: 23-38
- 2004
- [j29]Sara Negri, Jan von Plato, Thierry Coquand: Proof-theoretical analysis of order relations. Arch. Math. Log. 43(3): 297-310 (2004)
- [c26]
- 2003
- [j28]Thierry Coquand, Giovanni Sambin, Jan M. Smith, Silvio Valentini: Inductively generated formal topologies. Ann. Pure Appl. Logic 124(1-3): 71-106 (2003)
- [j27]Marc Bezem, Thierry Coquand: Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. Bulletin of the EATCS 79: 86-100 (2003)
- [j26]Thierry Coquand: A syntactical proof of the Marriage Lemma. Theor. Comput. Sci. 290(1): 1107-1113 (2003)
- [j25]Thierry Coquand, Guo-Qiang Zhang: A representation of stably compact spaces, and patch topology. Theor. Comput. Sci. 305(1-3): 77-84 (2003)
- [c25]
- [c24]Thierry Coquand, Randy Pollack, Makoto Takeyama: A Logical Framework with Dependently Typed Records. TLCA 2003: 105-119
- 2002
- [j24]Thierry Coquand, Erik Palmgren: Metric Boolean algebras and constructive measure theory. Arch. Math. Log. 41(7): 687-704 (2002)
- 2001
- [c23]Thorsten Altenkirch, Thierry Coquand: A Finitary Subsystem of the Polymorphic lambda-Calculus. TLCA 2001: 22-28
- 2000
- [j23]Thierry Coquand, Erik Palmgren: Intuitionistic choice and classical logic. Arch. Math. Log. 39(1): 53-74 (2000)
- [j22]Thierry Coquand, Sara Sadocco, Giovanni Sambin, Jan M. Smith: Formal Topologies on The Set of First-Order Formulae. J. Symb. Log. 65(3): 1183-1192 (2000)
- [c22]
- [c21]
- [c20]
- [e1]Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith (Eds.): Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers. Lecture Notes in Computer Science 1956, Springer 2000, ISBN 3-540-41517-3
1990 – 1999
- 1999
- [j21]
- [j20]Thierry Coquand: A Note on Formal Iterated Function Systems. Electr. Notes Theor. Comput. Sci. 24: 2-12 (1999)
- [j19]Thierry Coquand, Martin Hofmann: A new method for establishing conservativity of classical systems over their intuitionistic version. Mathematical Structures in Computer Science 9(4): 323-333 (1999)
- 1998
- [j18]
- [j17]Stefano Berardi, Marc Bezem, Thierry Coquand: On the Computational Content of the Axiom of Choice. J. Symb. Log. 63(2): 600-622 (1998)
- [c19]
- 1997
- [j16]
- [j15]Thierry Coquand, Peter Dybjer: Intuitionistic Model Constructions and Normalization Proofs. Mathematical Structures in Computer Science 7(1): 75-94 (1997)
- [c18]Thierry Coquand, Henrik Persson: A Proof-Theoretical Investigation of Zantema's Problem. CSL 1997: 177-188
- 1996
- [j14]Thierry Coquand: An Algorithm for Type-Checking Dependent Types. Sci. Comput. Program. 26(1-3): 167-177 (1996)
- 1995
- [j13]Thierry Coquand: A Semantics of Evidence for Classical Arithmetic. J. Symb. Log. 60(1): 325-337 (1995)
- [c17]
- [c16]Stefano Berardi, Marc Bezem, Thierry Coquand: A realization of the negative interpretation of the Axiom of Choice. TLCA 1995: 47-62
- [c15]
- 1994
- [j12]Thierry Coquand, Bengt Nordström, Jan M. Smith, Björn von Sydow: Type Theorie Programming. Bulletin of the EATCS 52: 203-228 (1994)
- [j11]
- [j10]Thierry Coquand, Hugo Herbelin: A - Translation and Looping Combinators in Pure Type Systems. J. Funct. Program. 4(1): 77-88 (1994)
- [c14]Thierry Coquand, Peter Dybjer: Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS 1994: 60-76
- 1993
- [j9]Thierry Coquand: Another Proof of the Intuitionistic Ramsey Theorem. Theor. Comput. Sci. 115(1): 63-75 (1993)
- [c13]
- 1992
- [j8]
- [j7]
- 1991
- [j6]Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov: Inheritance as Implicit Coercion. Inf. Comput. 93(1): 172-221 (1991)
- [c12]Thierry Coquand: Constructive Topology and Combinatorics. Constructivity in Computer Science 1991: 159-164
- [c11]Thierry Coquand: A Direct Proof of the Intuitionistic Ramsey Theorem. Category Theory and Computer Science 1991: 164-172
1980 – 1989
- 1989
- [j5]Thierry Coquand, Carl A. Gunter, Glynn Winskel: Domain Theoretic Models of Polymorphism. Inf. Comput. 81(2): 123-167 (1989)
- [j4]
- [c10]Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov: Inheritance and Explicit Coercion (Preliminary Report). LICS 1989: 112-129
- 1988
- [j3]
- [j2]Val Tannen, Thierry Coquand: Extensional Models for Polymorphism. Theor. Comput. Sci. 59: 85-114 (1988)
- [c9]Thierry Coquand, Christine Paulin: Inductively defined types. Conference on Computer Logic 1988: 50-66
- [c8]
- 1987
- [c7]Thierry Coquand, Thomas Ehrhard: An Equational Presentation of Higher Order Logic. Category Theory and Computer Science 1987: 40-56
- [c6]Thierry Coquand, Carl A. Gunter, Glynn Winskel: DI-Domains as a Model of Polymorphism. MFPS 1987: 344-363
- [c5]
- 1986
- [c4]
- 1985
- [j1]Thierry Coquand, Gérard P. Huet: A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. J. Symb. Comput. 1(3): 323-328 (1985)
- [c3]Thierry Coquand, Gérard P. Huet: Constructions: A Higher Order Proof System for Mechanizing Mathematics. European Conference on Computer Algebra (1) 1985: 151-184
- [c2]Thierry Coquand: Sur l'Analogie entre les Propositions et les Types. Combinators and Functional Programming Languages 1985: 71-84
- [c1]Thierry Coquand, Gérard P. Huet: Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Logic Colloquium 1985: 123-146
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-10-02 10:55 CEST by the dblp team