dblp.uni-trier.dewww.uni-trier.de

Thierry Coquand Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo

*2009
87EEThierry Coquand: Forcing and Type Theory. CSL 2009: 2
86EEAndreas Abel, Thierry Coquand, Miguel Pagano: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009: 5-19
85EEThierry Coquand: Space of valuations. Ann. Pure Appl. Logic 157(2-3): 97-109 (2009)
2008
84EEThierry Coquand: Constructive Mathematics and Functional Programming (Abstract). ESOP 2008: 146-147
83EEAndreas Abel, Thierry Coquand, Peter Dybjer: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13
82EEAndreas Abel, Thierry Coquand, Peter Dybjer: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56
81EEThierry Coquand, Henri Lombardi: A note on the axiomatisation of real numbers. Math. Log. Q. 54(3): 224-228 (2008)
2007
80EEThierry Coquand, Arnaud Spiwack: Towards Constructive Homological Algebra in Type Theory. Calculemus/MKM 2007: 40-54
79EEAndreas Abel, Thierry Coquand, Peter Dybjer: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12
78EEThierry Coquand, Arnaud Spiwack: A proof of strong normalisation using domain theory CoRR abs/0709.1401: (2007)
77EEThierry Coquand: The Completeness of Typing for Context-Semantics. Fundam. Inform. 77(4): 293-301 (2007)
76EEAndreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Inform. 77(4): 345-395 (2007)
75EEThierry 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
73EEThierry Coquand, Arnaud Spiwack: A Proof of Strong Normalisation using Domain Theory. LICS 2006: 307-316
72EEThierry Coquand: Alfa/Agda. The Seventeen Provers of the World 2006: 50-54
71EEBernhard Banaschewski, Thierry Coquand, Giovanni Sambin: Preface. Ann. Pure Appl. Logic 137(1-3): 1-2 (2006)
70EEGilles Barthe, Thierry Coquand: Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16(2): 137-155 (2006)
69EEThierry Coquand, Henri Lombardi: A logical approach to abstract algebra. Mathematical Structures in Computer Science 16(5): 885-900 (2006)
2005
68EEThierry Coquand: A Logical Approach to Abstract Algebra. CiE 2005: 86-95
67EEAndreas 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
65EEMarc Bezem, Thierry Coquand: Automating Coherent Logic. LPAR 2005: 246-260
64EEThierry Coquand, Henri Lombardi, Marie-Françoise Roy: 05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005
63EEThierry Coquand: 05021 Executive Summary -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005
62EEThierry Coquand, Henri Lombardi, Peter Schuster: A Nilregular Element Property. Mathematics, Algorithms, Proofs 2005
61EEThierry Coquand: Completeness Theorems and lambda-Calculus. TLCA 2005: 1-9
60EEAndreas Abel, Thierry Coquand: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA 2005: 23-38
59EEThierry Coquand, Randy Pollack, Makoto Takeyama: A Logical Framework with Dependently Typed Records. Fundam. Inform. 65(1-2): 113-134 (2005)
58EEThierry Coquand, Bas Spitters: Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. UCS 11(12): 1932-1944 (2005)
57EEThierry Coquand, Bas Spitters: A constructive proof of the Peter-Weyl theorem. Math. Log. Q. 51(4): 351-359 (2005)
2004
56EEAna Bove, Thierry Coquand: Formalising Bitonic Sort in Type Theory. TYPES 2004: 82-97
55EESara Negri, Jan von Plato, Thierry Coquand: Proof-theoretical analysis of order relations. Arch. Math. Log. 43(3): 297-310 (2004)
2003
54EEThierry Coquand: Dynamical Method in Algebra: A Survey. TABLEAUX 2003: 2
53EEThierry Coquand, Randy Pollack, Makoto Takeyama: A Logical Framework with Dependently Typed Records. TLCA 2003: 105-119
52EEThierry 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)
49EEThierry Coquand, Guo-Qiang Zhang: A representation of stably compact spaces, and patch topology. Theor. Comput. Sci. 305(1-3): 77-84 (2003)
2002
48EEThierry Coquand, Erik Palmgren: Metric Boolean algebras and constructive measure theory. Arch. Math. Log. 41(7): 687-704 (2002)
2001
47EEThorsten 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
45EEGilles Barthe, Thierry Coquand: An Introduction to Dependent Type Theory. APPSEM 2000: 1-41
44EEThierry Coquand, Guo-Qiang Zhang: Sequents, Frames, and Completeness. CSL 2000: 277-291
43EEThierry Coquand, Makoto Takeyama: An Implementation of Type: Type. TYPES 2000: 53-62
42EEThierry 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)
39EEThierry 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
37EEThierry Coquand, Henrik Persson: Gröbner Bases in Type Theory. TYPES 1998: 33-46
36EEThierry 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
34EEThierry 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
28EEThierry 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
26EEThierry 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
12EEThierry 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
7EEThierry Coquand, Carl A. Gunter, Glynn Winskel: DI-Domains as a Model of Polymorphism. MFPS 1987: 344-363
6EEVal 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
4EEThierry 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

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

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)