| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster |
Preface.  |
Ann. Pure Appl. Logic  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Erik Palmgren, Bas Spitters |
Metric complements of overt closed sets. |
Math. Log. Q. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Vincent Siles |
A Decision Procedure for Regular Expression Equivalence in Type Theory. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi, Claude Quitté |
Curves and coherent Prüfer rings. |
J. Symb. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Thierry Coquand, Susumu Hayashi |
Games with 1-backtracking. |
Ann. Pure Appl. Logic |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Guilhem Jaber |
A Note on Forcing and Type Theory. |
Fundam. Inform. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Space of valuations. |
Ann. Pure Appl. Logic |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi, Peter Schuster |
Spectral schemes as ringed lattices. |
Ann. Math. Artif. Intell. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand, Miguel Pagano |
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Forcing and Type Theory. |
CSL |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi |
A note on the axiomatisation of real numbers. |
Math. Log. Q. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand, Peter Dybjer |
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. |
FLOPS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand, Peter Dybjer |
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. |
MPC |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Constructive Mathematics and Functional Programming (Abstract). |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Arnaud Spiwack |
A proof of strong normalisation using domain theory. |
Logical Methods in Computer Science |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
The Completeness of Typing for Context-Semantics. |
Fundam. Inform. |
2007 |
DBLP BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand |
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. |
Fundam. Inform. |
2007 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Arnaud Spiwack |
A proof of strong normalisation using domain theory |
CoRR |
2007 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Arnaud Spiwack |
Towards Constructive Homological Algebra in Type Theory. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand, Peter Dybjer |
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. |
LICS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi |
A logical approach to abstract algebra. |
Mathematical Structures in Computer Science |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Banaschewski, Thierry Coquand, Giovanni Sambin |
Preface. |
Ann. Pure Appl. Logic |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Thierry Coquand |
Remarks on the equational theory of non-normalizing pure type systems. |
J. Funct. Program. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi, Marie-Françoise Roy (eds.) |
Mathematics, Algorithms, Proofs, 9.-14. January 2005 |
Mathematics, Algorithms, Proofs |
2006 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand |
Alfa/Agda. |
The Seventeen Provers of the World |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Arnaud Spiwack |
A Proof of Strong Normalisation using Domain Theory. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Bas Spitters |
A constructive proof of the Peter-Weyl theorem. |
Math. Log. Q. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Bas Spitters |
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. |
J. UCS |
2005 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Randy Pollack, Makoto Takeyama |
A Logical Framework with Dependently Typed Records. |
Fundam. Inform. |
2005 |
DBLP BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand |
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Completeness Theorems and lambda-Calculus. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Thierry Coquand, Susumu Hayashi |
Games with 1-backtracking. |
GALOP |
2005 |
DBLP BibTeX RDF |
|
| 1 | Marc Bezem, Thierry Coquand |
Automating Coherent Logic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi, Peter Schuster |
A Nilregular Element Property. |
Mathematics, Algorithms, Proofs |
2005 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand |
05021 Executive Summary -- Mathematics, Algorithms, Proofs. |
Mathematics, Algorithms, Proofs |
2005 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Henri Lombardi, Marie-Françoise Roy |
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. |
Mathematics, Algorithms, Proofs |
2005 |
DBLP BibTeX RDF |
|
| 1 | Andreas Abel, Thierry Coquand, Ulf Norell |
Connecting a Logical Framework to a First-Order Logic Prover. |
FroCos |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
A Logical Approach to Abstract Algebra. |
CiE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sara Negri, Jan von Plato, Thierry Coquand |
Proof-theoretical analysis of order relations. |
Arch. Math. Log. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Bove, Thierry Coquand |
Formalising Bitonic Sort in Type Theory. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
A syntactical proof of the Marriage Lemma. |
Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Guo-Qiang Zhang |
A representation of stably compact spaces, and patch topology. |
Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Giovanni Sambin, Jan M. Smith, Silvio Valentini |
Inductively generated formal topologies. |
Ann. Pure Appl. Logic |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2003 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Randy Pollack, Makoto Takeyama |
A Logical Framework with Dependently Typed Records. |
TLCA |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Dynamical Method in Algebra: A Survey. |
TABLEAUX |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Erik Palmgren |
Metric Boolean algebras and constructive measure theory. |
Arch. Math. Log. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch, Thierry Coquand |
A Finitary Subsystem of the Polymorphic lambda-Calculus. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Sara Sadocco, Giovanni Sambin, Jan M. Smith |
Formal Topologies on The Set of First-Order Formulae. |
J. Symb. Log. |
2000 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Erik Palmgren |
Intuitionistic choice and classical logic. |
Arch. Math. Log. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
TYPES |
2000 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Makoto Takeyama |
An Implementation of Type: Type. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Guo-Qiang Zhang |
Sequents, Frames, and Completeness. |
CSL |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Thierry Coquand |
An Introduction to Dependent Type Theory. |
APPSEM |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Martin Hofmann |
A new method for establishing conservativity of classical systems over their intuitionistic version. |
Mathematical Structures in Computer Science |
1999 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand |
A Note on Formal Iterated Function Systems. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
A Boolean Model of Ultrafilters. |
Ann. Pure Appl. Logic |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Marc Bezem, Thierry Coquand |
On the Computational Content of the Axiom of Choice. |
J. Symb. Log. |
1998 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand |
Two applications of Boolean models. |
Arch. Math. Log. |
1998 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classification (1991): 03F55, 03F65, 03G05 |
| 1 | Thierry Coquand, Henrik Persson |
Gröbner Bases in Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Peter Dybjer |
Intuitionistic Model Constructions and Normalization Proofs. |
Mathematical Structures in Computer Science |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Minimal Invariant Spaces in Formal Topology. |
J. Symb. Log. |
1997 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Henrik Persson |
A Proof-Theoretical Investigation of Zantema's Problem. |
CSL |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
An Algorithm for Type-Checking Dependent Types. |
Sci. Comput. Program. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
A Semantics of Evidence for Classical Arithmetic. |
J. Symb. Log. |
1995 |
DBLP BibTeX RDF |
|
| 1 | Stefano Berardi, Marc Bezem, Thierry Coquand |
A realization of the negative interpretation of the Axiom of Choice. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Jan M. Smith |
An Application of Constructive Completeness. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Program Construction in Intuitionistic Type Theory (Abstract). |
MPC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
An Analysis of Ramsey's Theorem |
Inf. Comput. |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Bengt Nordström, Jan M. Smith, Björn von Sydow |
Type Theorie Programming. |
Bulletin of the EATCS |
1994 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Hugo Herbelin |
A - Translation and Looping Combinators in Pure Type Systems. |
J. Funct. Program. |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Peter Dybjer |
Inductive Definitions and Type Theory: an Introduction (Preliminary Version). |
FSTTCS |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Another Proof of the Intuitionistic Ramsey Theorem. |
Theor. Comput. Sci. |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Infinite Objects in Type Theory. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
An Intuitionistic Proof of Tychonoff's Theorem. |
J. Symb. Log. |
1992 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand |
The Paradox of Trees in Type Theory. |
BIT |
1992 |
DBLP BibTeX RDF |
|
| 1 | Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov |
Inheritance as Implicit Coercion |
Inf. Comput. |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Constructive Topology and Combinatorics. |
Constructivity in Computer Science |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
A Direct Proof of the Intuitionistic Ramsey Theorem. |
Category Theory and Computer Science |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Categories of Embeddings. |
Theor. Comput. Sci. |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Carl A. Gunter, Glynn Winskel |
Domain Theoretic Models of Polymorphism |
Inf. Comput. |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov |
Inheritance and Explicit Coercion (Preliminary Report) |
LICS |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Val Tannen, Thierry Coquand |
Extensional Models for Polymorphism. |
Theor. Comput. Sci. |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Gérard P. Huet |
The Calculus of Constructions |
Inf. Comput. |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Christine Paulin |
Inductively defined types. |
Conference on Computer Logic |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Categories of Embeddings |
LICS |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Carl A. Gunter, Glynn Winskel |
DI-Domains as a Model of Polymorphism. |
MFPS |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Val Tannen, Thierry Coquand |
Extensional Models for Polymorphism. |
TAPSOFT, Vol.2 |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Thomas Ehrhard |
An Equational Presentation of Higher Order Logic. |
Category Theory and Computer Science |
1987 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
An Analysis of Girard's Paradox |
LICS |
1986 |
DBLP BibTeX RDF |
|
| 1 | Thierry Coquand, Gérard P. Huet |
A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. |
J. Symb. Comput. |
1985 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand |
Sur l'Analogie entre les Propositions et les Types. |
Combinators and Functional Programming Languages |
1985 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Gérard P. Huet |
Constructions: A Higher Order Proof System for Mechanizing Mathematics. |
European Conference on Computer Algebra |
1985 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Gérard P. Huet |
Concepts mathématiques et informatiques formalisés dans le calcul des constructions. |
Logic Colloquium |
1985 |
DBLP BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")