 | 2009 |
|---|
| 87 |       | Thierry Coquand:
Forcing and Type Theory.
CSL 2009: 2 |
| 86 | | Andreas Abel,
Thierry Coquand,
Miguel Pagano:
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance.
TLCA 2009: 5-19 |
| 85 | | Thierry Coquand:
Space of valuations.
Ann. Pure Appl. Logic 157(2-3): 97-109 (2009) |
| 2008 |
|---|
| 84 | | Thierry Coquand:
Constructive Mathematics and Functional Programming (Abstract).
ESOP 2008: 146-147 |
| 83 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.
FLOPS 2008: 3-13 |
| 82 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.
MPC 2008: 29-56 |
| 81 | | Thierry Coquand,
Henri Lombardi:
A note on the axiomatisation of real numbers.
Math. Log. Q. 54(3): 224-228 (2008) |
| 2007 |
|---|
| 80 | | Thierry Coquand,
Arnaud Spiwack:
Towards Constructive Homological Algebra in Type Theory.
Calculemus/MKM 2007: 40-54 |
| 79 | | Andreas Abel,
Thierry Coquand,
Peter Dybjer:
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.
LICS 2007: 3-12 |
| 78 | | Thierry Coquand,
Arnaud Spiwack:
A proof of strong normalisation using domain theory
CoRR abs/0709.1401: (2007) |
| 77 | | Thierry Coquand:
The Completeness of Typing for Context-Semantics.
Fundam. Inform. 77(4): 293-301 (2007) |
| 76 | | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
Fundam. Inform. 77(4): 345-395 (2007) |
| 75 | | Thierry Coquand,
Arnaud Spiwack:
A proof of strong normalisation using domain theory.
Logical Methods in Computer Science 3(4): (2007) |
| 2006 |
|---|
| 74 |  | Thierry Coquand,
Henri Lombardi,
Marie-Françoise Roy:
Mathematics, Algorithms, Proofs, 9.-14. January 2005
Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006 |
| 73 | | Thierry Coquand,
Arnaud Spiwack:
A Proof of Strong Normalisation using Domain Theory.
LICS 2006: 307-316 |
| 72 | | Thierry Coquand:
Alfa/Agda.
The Seventeen Provers of the World 2006: 50-54 |
| 71 | | Bernhard Banaschewski,
Thierry Coquand,
Giovanni Sambin:
Preface.
Ann. Pure Appl. Logic 137(1-3): 1-2 (2006) |
| 70 | | Gilles Barthe,
Thierry Coquand:
Remarks on the equational theory of non-normalizing pure type systems.
J. Funct. Program. 16(2): 137-155 (2006) |
| 69 | | Thierry Coquand,
Henri Lombardi:
A logical approach to abstract algebra.
Mathematical Structures in Computer Science 16(5): 885-900 (2006) |
| 2005 |
|---|
| 68 | | Thierry Coquand:
A Logical Approach to Abstract Algebra.
CiE 2005: 86-95 |
| 67 | | Andreas Abel,
Thierry Coquand,
Ulf Norell:
Connecting a Logical Framework to a First-Order Logic Prover.
FroCos 2005: 285-301 |
| 66 | | Stefano Berardi,
Thierry Coquand,
Susumu Hayashi:
Games with 1-backtracking.
GALOP 2005: 210-225 |
| 65 | | Marc Bezem,
Thierry Coquand:
Automating Coherent Logic.
LPAR 2005: 246-260 |
| 64 | | Thierry Coquand,
Henri Lombardi,
Marie-Françoise Roy:
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs.
Mathematics, Algorithms, Proofs 2005 |
| 63 | | Thierry Coquand:
05021 Executive Summary -- Mathematics, Algorithms, Proofs.
Mathematics, Algorithms, Proofs 2005 |
| 62 | | Thierry Coquand,
Henri Lombardi,
Peter Schuster:
A Nilregular Element Property.
Mathematics, Algorithms, Proofs 2005 |
| 61 | | Thierry Coquand:
Completeness Theorems and lambda-Calculus.
TLCA 2005: 1-9 |
| 60 | | Andreas Abel,
Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
TLCA 2005: 23-38 |
| 59 | | Thierry Coquand,
Randy Pollack,
Makoto Takeyama:
A Logical Framework with Dependently Typed Records.
Fundam. Inform. 65(1-2): 113-134 (2005) |
| 58 | | Thierry Coquand,
Bas Spitters:
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems.
J. UCS 11(12): 1932-1944 (2005) |
| 57 | | Thierry Coquand,
Bas Spitters:
A constructive proof of the Peter-Weyl theorem.
Math. Log. Q. 51(4): 351-359 (2005) |
| 2004 |
|---|
| 56 | | Ana Bove,
Thierry Coquand:
Formalising Bitonic Sort in Type Theory.
TYPES 2004: 82-97 |
| 55 | | Sara Negri,
Jan von Plato,
Thierry Coquand:
Proof-theoretical analysis of order relations.
Arch. Math. Log. 43(3): 297-310 (2004) |
| 2003 |
|---|
| 54 | | Thierry Coquand:
Dynamical Method in Algebra: A Survey.
TABLEAUX 2003: 2 |
| 53 | | Thierry Coquand,
Randy Pollack,
Makoto Takeyama:
A Logical Framework with Dependently Typed Records.
TLCA 2003: 105-119 |
| 52 | | Thierry Coquand,
Giovanni Sambin,
Jan M. Smith,
Silvio Valentini:
Inductively generated formal topologies.
Ann. Pure Appl. Logic 124(1-3): 71-106 (2003) |
| 51 | | 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) |
| 50 | | Thierry Coquand:
A syntactical proof of the Marriage Lemma.
Theor. Comput. Sci. 290(1): 1107-1113 (2003) |
| 49 | | Thierry Coquand,
Guo-Qiang Zhang:
A representation of stably compact spaces, and patch topology.
Theor. Comput. Sci. 305(1-3): 77-84 (2003) |
| 2002 |
|---|
| 48 | | Thierry Coquand,
Erik Palmgren:
Metric Boolean algebras and constructive measure theory.
Arch. Math. Log. 41(7): 687-704 (2002) |
| 2001 |
|---|
| 47 | | Thorsten Altenkirch,
Thierry Coquand:
A Finitary Subsystem of the Polymorphic lambda-Calculus.
TLCA 2001: 22-28 |
| 2000 |
|---|
| 46 | | Thierry Coquand,
Peter Dybjer,
Bengt Nordström,
Jan M. Smith:
Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers
Springer 2000 |
| 45 | | Gilles Barthe,
Thierry Coquand:
An Introduction to Dependent Type Theory.
APPSEM 2000: 1-41 |
| 44 | | Thierry Coquand,
Guo-Qiang Zhang:
Sequents, Frames, and Completeness.
CSL 2000: 277-291 |
| 43 | | Thierry Coquand,
Makoto Takeyama:
An Implementation of Type: Type.
TYPES 2000: 53-62 |
| 42 | | Thierry Coquand,
Erik Palmgren:
Intuitionistic choice and classical logic.
Arch. Math. Log. 39(1): 53-74 (2000) |
| 41 | | 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) |
| 1999 |
|---|
| 40 | | Thierry Coquand:
A Boolean Model of Ultrafilters.
Ann. Pure Appl. Logic 99(1-3): 231-239 (1999) |
| 39 | | Thierry Coquand:
A Note on Formal Iterated Function Systems.
Electr. Notes Theor. Comput. Sci. 24: (1999) |
| 38 | | 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 |
|---|
| 37 | | Thierry Coquand,
Henrik Persson:
Gröbner Bases in Type Theory.
TYPES 1998: 33-46 |
| 36 | | Thierry Coquand:
Two applications of Boolean models.
Arch. Math. Log. 37(3): 143-147 (1998) |
| 35 | | Stefano Berardi,
Marc Bezem,
Thierry Coquand:
On the Computational Content of the Axiom of Choice.
J. Symb. Log. 63(2): 600-622 (1998) |
| 1997 |
|---|
| 34 | | Thierry Coquand,
Henrik Persson:
A Proof-Theoretical Investigation of Zantema's Problem.
CSL 1997: 177-188 |
| 33 | | Thierry Coquand:
Minimal Invariant Spaces in Formal Topology.
J. Symb. Log. 62(3): 689-698 (1997) |
| 32 | | Thierry Coquand,
Peter Dybjer:
Intuitionistic Model Constructions and Normalization Proofs.
Mathematical Structures in Computer Science 7(1): 75-94 (1997) |
| 1996 |
|---|
| 31 | | Thierry Coquand:
An Algorithm for Type-Checking Dependent Types.
Sci. Comput. Program. 26(1-3): 167-177 (1996) |
| 1995 |
|---|
| 30 | | Thierry Coquand:
Program Construction in Intuitionistic Type Theory (Abstract).
MPC 1995: 49 |
| 29 | | Stefano Berardi,
Marc Bezem,
Thierry Coquand:
A realization of the negative interpretation of the Axiom of Choice.
TLCA 1995: 47-62 |
| 28 | | Thierry Coquand,
Jan M. Smith:
An Application of Constructive Completeness.
TYPES 1995: 76-84 |
| 27 | | Thierry Coquand:
A Semantics of Evidence for Classical Arithmetic.
J. Symb. Log. 60(1): 325-337 (1995) |
| 1994 |
|---|
| 26 | | Thierry Coquand,
Peter Dybjer:
Inductive Definitions and Type Theory: an Introduction (Preliminary Version).
FSTTCS 1994: 60-76 |
| 25 | | Thierry Coquand,
Bengt Nordström,
Jan M. Smith,
Björn von Sydow:
Type Theorie Programming.
Bulletin of the EATCS 52: 203-228 (1994) |
| 24 | | Thierry Coquand:
An Analysis of Ramsey's Theorem
Inf. Comput. 110(2): 297-304 (1994) |
| 23 | | Thierry Coquand,
Hugo Herbelin:
A - Translation and Looping Combinators in Pure Type Systems.
J. Funct. Program. 4(1): 77-88 (1994) |
| 1993 |
|---|
| 22 | | Thierry Coquand:
Infinite Objects in Type Theory.
TYPES 1993: 62-78 |
| 21 | | Thierry Coquand:
Another Proof of the Intuitionistic Ramsey Theorem.
Theor. Comput. Sci. 115(1): 63-75 (1993) |
| 1992 |
|---|
| 20 | | Thierry Coquand:
The Paradox of Trees in Type Theory.
BIT 32(1): 10-14 (1992) |
| 19 | | Thierry Coquand:
An Intuitionistic Proof of Tychonoff's Theorem.
J. Symb. Log. 57(1): 28-32 (1992) |
| 1991 |
|---|
| 18 | | Thierry Coquand:
A Direct Proof of the Intuitionistic Ramsey Theorem.
Category Theory and Computer Science 1991: 164-172 |
| 17 | | Thierry Coquand:
Constructive Topology and Combinatorics.
Constructivity in Computer Science 1991: 159-164 |
| 16 | | Val Tannen,
Thierry Coquand,
Carl A. Gunter,
Andre Scedrov:
Inheritance as Implicit Coercion
Inf. Comput. 93(1): 172-221 (1991) |
| 1989 |
|---|
| 15 | | Val Tannen,
Thierry Coquand,
Carl A. Gunter,
Andre Scedrov:
Inheritance and Explicit Coercion (Preliminary Report)
LICS 1989: 112-129 |
| 14 | | Thierry Coquand,
Carl A. Gunter,
Glynn Winskel:
Domain Theoretic Models of Polymorphism
Inf. Comput. 81(2): 123-167 (1989) |
| 13 | | Thierry Coquand:
Categories of Embeddings.
Theor. Comput. Sci. 68(3): 221-237 (1989) |
| 1988 |
|---|
| 12 | | Thierry Coquand,
Christine Paulin:
Inductively defined types.
Conference on Computer Logic 1988: 50-66 |
| 11 | | Thierry Coquand:
Categories of Embeddings
LICS 1988: 256-263 |
| 10 | | Thierry Coquand,
Gérard P. Huet:
The Calculus of Constructions
Inf. Comput. 76(2/3): 95-120 (1988) |
| 9 | | Val Tannen,
Thierry Coquand:
Extensional Models for Polymorphism.
Theor. Comput. Sci. 59: 85-114 (1988) |
| 1987 |
|---|
| 8 | | Thierry Coquand,
Thomas Ehrhard:
An Equational Presentation of Higher Order Logic.
Category Theory and Computer Science 1987: 40-56 |
| 7 | | Thierry Coquand,
Carl A. Gunter,
Glynn Winskel:
DI-Domains as a Model of Polymorphism.
MFPS 1987: 344-363 |
| 6 | | Val Tannen,
Thierry Coquand:
Extensional Models for Polymorphism.
TAPSOFT, Vol.2 1987: 291-307 |
| 1986 |
|---|
| 5 | | Thierry Coquand:
An Analysis of Girard's Paradox
LICS 1986: 227-236 |
| 1985 |
|---|
| 4 | | Thierry Coquand:
Sur l'Analogie entre les Propositions et les Types.
Combinators and Functional Programming Languages 1985: 71-84 |
| 3 | | Thierry Coquand,
Gérard P. Huet:
Constructions: A Higher Order Proof System for Mechanizing Mathematics.
European Conference on Computer Algebra (1) 1985: 151-184 |
| 2 | | Thierry Coquand,
Gérard P. Huet:
Concepts mathématiques et informatiques formalisés dans le calcul des constructions.
Logic Colloquium 1985: 123-146 |
| 1 | | 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) |
