Thierry Coquand

	2012
95		Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster: Preface. Ann. Pure Appl. Logic 163(2): 85-86 (2012)
	2011
94		Thierry Coquand, Vincent Siles: A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP 2011: 119-134
93		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)
92		Thierry Coquand, Erik Palmgren, Bas Spitters: Metric complements of overt closed sets. Math. Log. Q. 57(4): 373-378 (2011)
	2010
91		Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. Ann. Pure Appl. Logic 161(10): 1254-1269 (2010)
90		Thierry Coquand, Guilhem Jaber: A Note on Forcing and Type Theory. Fundam. Inform. 100(1-4): 43-52 (2010)
89		Thierry Coquand, Henri Lombardi, Claude Quitté: Curves and coherent Prüfer rings. J. Symb. Comput. 45(12): 1378-1390 (2010)
	2009
88		Thierry Coquand: Forcing and Type Theory. CSL 2009: 2
87		Andreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009: 5-19
86		Thierry Coquand, Henri Lombardi, Peter Schuster: Spectral schemes as ringed lattices. Ann. Math. Artif. Intell. 56(3-4): 339-360 (2009)
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: 2-12 (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)

Coauthor Index

1	Andreas Abel	[60] [67] [76] [79] [82] [83] [87] [93]
2	Thorsten Altenkirch	[47]
3	Bernhard Banaschewski	[71]
4	Gilles Barthe	[45] [70]
5	Andrej Bauer	[95]
6	Stefano Berardi	[29] [35] [66] [91]
7	Marc Bezem	[29] [35] [51] [65]
8	Ana Bove	[56]
9	Peter Dybjer	[26] [32] [46] [79] [82] [83]
10	Thomas Ehrhard	[8]
11	Carl A. Gunter	[7] [14] [15] [16]
12	Susumu Hayashi	[66] [91]
13	Hugo Herbelin	[23]
14	Martin Hofmann	[38]
15	Gérard P. Huet	[1] [2] [3] [10]
16	Guilhem Jaber	[90]
17	Henri Lombardi	[62] [64] [69] [74] [81] [86] [89]
18	Sara Negri	[55]
19	Bengt Nordström	[25] [46]
20	Ulf Norell	[67]
21	Miguel Pagano	[87] [93]
22	Erik Palmgren	[42] [48] [92]
23	Christine Paulin	[12]
24	Henrik Persson	[34] [37]
25	Jan von Plato	[55]
26	Randy Pollack	[53] [59]
27	Claude Quitté	[89]
28	Marie-Françoise Roy	[64] [74]
29	Sara Sadocco	[41]
30	Giovanni Sambin	[41] [52] [71] [95]
31	Andre Scedrov	[15] [16]
32	Peter Schuster (Peter M. Schuster)	[62] [86] [95]
33	Vincent Siles	[94]
34	Jan M. Smith	[25] [28] [41] [46] [52]
35	Bas Spitters	[57] [58] [92]
36	Arnaud Spiwack	[73] [75] [78] [80]
37	Björn von Sydow	[25]
38	Makoto Takeyama	[43] [53] [59]
39	Val Tannen (Valeriu Breazu, Val Breazu-Tannen)	[6] [9] [15] [16]
40	Silvio Valentini	[52]
41	Glynn Winskel	[7] [14]
42	Guo-Qiang Zhang	[44] [49]

Colors in the list of coauthors

Last update Tue May 29 01:28:40 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page