Search the dblp DataBase
Thierry Coquand :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Val Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov Inheritance and Explicit Coercion (Preliminary Report) [Citation Graph (1, 0)][DBLP ] LICS, 1989, pp:112-129 [Conf ] Val Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov Inheritance as Implicit Coercion [Citation Graph (1, 0)][DBLP ] Inf. Comput., 1991, v:93, n:1, pp:172-221 [Journal ] Gilles Barthe , Thierry Coquand An Introduction to Dependent Type Theory. [Citation Graph (0, 0)][DBLP ] APPSEM, 2000, pp:1-41 [Conf ] Thierry Coquand A Logical Approach to Abstract Algebra. [Citation Graph (0, 0)][DBLP ] CiE, 2005, pp:86-95 [Conf ] Thierry Coquand , Christine Paulin Inductively defined types. [Citation Graph (0, 0)][DBLP ] Conference on Computer Logic, 1988, pp:50-66 [Conf ] Thierry Coquand Constructive Topology and Combinatorics. [Citation Graph (0, 0)][DBLP ] Constructivity in Computer Science, 1991, pp:159-164 [Conf ] Thierry Coquand , Henrik Persson A Proof-Theoretical Investigation of Zantema's Problem. [Citation Graph (0, 0)][DBLP ] CSL, 1997, pp:177-188 [Conf ] Thierry Coquand , Guo-Qiang Zhang Sequents, Frames, and Completeness. [Citation Graph (0, 0)][DBLP ] CSL, 2000, pp:277-291 [Conf ] Thierry Coquand A Direct Proof of the Intuitionistic Ramsey Theorem. [Citation Graph (0, 0)][DBLP ] Category Theory and Computer Science, 1991, pp:164-172 [Conf ] Thierry Coquand , Thomas Ehrhard An Equational Presentation of Higher Order Logic. [Citation Graph (0, 0)][DBLP ] Category Theory and Computer Science, 1987, pp:40-56 [Conf ] Thierry Coquand 05021 Executive Summary -- Mathematics, Algorithms, Proofs. [Citation Graph (0, 0)][DBLP ] Mathematics, Algorithms, Proofs, 2005, pp:- [Conf ] Thierry Coquand , Henri Lombardi , Marie-Françoise Roy 05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. [Citation Graph (0, 0)][DBLP ] Mathematics, Algorithms, Proofs, 2005, pp:- [Conf ] Thierry Coquand , Henri Lombardi , Peter Schuster A Nilregular Element Property. [Citation Graph (0, 0)][DBLP ] Mathematics, Algorithms, Proofs, 2005, pp:- [Conf ] Thierry Coquand , Gérard P. Huet Constructions: A Higher Order Proof System for Mechanizing Mathematics. [Citation Graph (0, 0)][DBLP ] European Conference on Computer Algebra (1), 1985, pp:151-184 [Conf ] Andreas Abel , Thierry Coquand , Ulf Norell Connecting a Logical Framework to a First-Order Logic Prover. [Citation Graph (0, 0)][DBLP ] FroCos, 2005, pp:285-301 [Conf ] Thierry Coquand , Peter Dybjer Inductive Definitions and Type Theory: an Introduction (Preliminary Version). [Citation Graph (0, 0)][DBLP ] FSTTCS, 1994, pp:60-76 [Conf ] Stefano Berardi , Thierry Coquand , Susumu Hayashi Games with 1-backtracking. [Citation Graph (0, 0)][DBLP ] GALOP, 2005, pp:210-225 [Conf ] Thierry Coquand An Analysis of Girard's Paradox [Citation Graph (0, 0)][DBLP ] LICS, 1986, pp:227-236 [Conf ] Thierry Coquand Categories of Embeddings [Citation Graph (0, 0)][DBLP ] LICS, 1988, pp:256-263 [Conf ] Thierry Coquand , Arnaud Spiwack A Proof of Strong Normalisation using Domain Theory. [Citation Graph (0, 0)][DBLP ] LICS, 2006, pp:307-316 [Conf ] Thierry Coquand Sur l'Analogie entre les Propositions et les Types. [Citation Graph (0, 0)][DBLP ] Combinators and Functional Programming Languages, 1985, pp:71-84 [Conf ] Thierry Coquand , Gérard P. Huet Concepts mathématiques et informatiques formalisés dans le calcul des constructions. [Citation Graph (0, 0)][DBLP ] Logic Colloquium, 1985, pp:123-146 [Conf ] Marc Bezem , Thierry Coquand Automating Coherent Logic. [Citation Graph (0, 0)][DBLP ] LPAR, 2005, pp:246-260 [Conf ] Thierry Coquand , Carl A. Gunter , Glynn Winskel DI-Domains as a Model of Polymorphism. [Citation Graph (0, 0)][DBLP ] MFPS, 1987, pp:344-363 [Conf ] Thierry Coquand Program Construction in Intuitionistic Type Theory (Abstract). [Citation Graph (0, 0)][DBLP ] MPC, 1995, pp:49- [Conf ] Thierry Coquand Dynamical Method in Algebra: A Survey. [Citation Graph (0, 0)][DBLP ] TABLEAUX, 2003, pp:2- [Conf ] Val Tannen , Thierry Coquand Extensional Models for Polymorphism. [Citation Graph (0, 0)][DBLP ] TAPSOFT, Vol.2, 1987, pp:291-307 [Conf ] Andreas Abel , Thierry Coquand Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. [Citation Graph (0, 0)][DBLP ] TLCA, 2005, pp:23-38 [Conf ] Thorsten Altenkirch , Thierry Coquand A Finitary Subsystem of the Polymorphic lambda-Calculus. [Citation Graph (0, 0)][DBLP ] TLCA, 2001, pp:22-28 [Conf ] Stefano Berardi , Marc Bezem , Thierry Coquand A realization of the negative interpretation of the Axiom of Choice. [Citation Graph (0, 0)][DBLP ] TLCA, 1995, pp:47-62 [Conf ] Thierry Coquand Completeness Theorems and lambda-Calculus. [Citation Graph (0, 0)][DBLP ] TLCA, 2005, pp:1-9 [Conf ] Thierry Coquand , Randy Pollack , Makoto Takeyama A Logical Framework with Dependently Typed Records. [Citation Graph (0, 0)][DBLP ] TLCA, 2003, pp:105-119 [Conf ] Thierry Coquand Alfa/Agda. [Citation Graph (0, 0)][DBLP ] The Seventeen Provers of the World, 2006, pp:50-54 [Conf ] Ana Bove , Thierry Coquand Formalising Bitonic Sort in Type Theory. [Citation Graph (0, 0)][DBLP ] TYPES, 2004, pp:82-97 [Conf ] Thierry Coquand Infinite Objects in Type Theory. [Citation Graph (0, 0)][DBLP ] TYPES, 1993, pp:62-78 [Conf ] Thierry Coquand , Henrik Persson Gröbner Bases in Type Theory. [Citation Graph (0, 0)][DBLP ] TYPES, 1998, pp:33-46 [Conf ] Thierry Coquand , Jan M. Smith An Application of Constructive Completeness. [Citation Graph (0, 0)][DBLP ] TYPES, 1995, pp:76-84 [Conf ] Thierry Coquand , Makoto Takeyama An Implementation of Type: Type. [Citation Graph (0, 0)][DBLP ] TYPES, 2000, pp:53-62 [Conf ] Sara Negri , Jan von Plato , Thierry Coquand Proof-theoretical analysis of order relations. [Citation Graph (0, 0)][DBLP ] Arch. Math. Log., 2004, v:43, n:3, pp:297-310 [Journal ] Bernhard Banaschewski , Thierry Coquand , Giovanni Sambin Preface. [Citation Graph (0, 0)][DBLP ] Ann. Pure Appl. Logic, 2006, v:137, n:1-3, pp:1-2 [Journal ] Thierry Coquand A Boolean Model of Ultrafilters. [Citation Graph (0, 0)][DBLP ] Ann. Pure Appl. Logic, 1999, v:99, n:1-3, pp:231-239 [Journal ] Thierry Coquand , Giovanni Sambin , Jan M. Smith , Silvio Valentini Inductively generated formal topologies. [Citation Graph (0, 0)][DBLP ] Ann. Pure Appl. Logic, 2003, v:124, n:1-3, pp:71-106 [Journal ] Thierry Coquand The Paradox of Trees in Type Theory. [Citation Graph (0, 0)][DBLP ] BIT, 1992, v:32, n:1, pp:10-14 [Journal ] Marc Bezem , Thierry Coquand Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. [Citation Graph (0, 0)][DBLP ] Bulletin of the EATCS, 2003, v:79, n:, pp:86-100 [Journal ] Thierry Coquand , Bengt Nordström , Jan M. Smith , Björn von Sydow Type Theorie Programming. [Citation Graph (0, 0)][DBLP ] Bulletin of the EATCS, 1994, v:52, n:, pp:203-228 [Journal ] Thierry Coquand A Note on Formal Iterated Function Systems. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:24, n:, pp:- [Journal ] Thierry Coquand , Randy Pollack , Makoto Takeyama A Logical Framework with Dependently Typed Records. [Citation Graph (0, 0)][DBLP ] Fundam. Inform., 2005, v:65, n:1-2, pp:113-134 [Journal ] Thierry Coquand An Analysis of Ramsey's Theorem [Citation Graph (0, 0)][DBLP ] Inf. Comput., 1994, v:110, n:2, pp:297-304 [Journal ] Thierry Coquand , Carl A. Gunter , Glynn Winskel Domain Theoretic Models of Polymorphism [Citation Graph (0, 0)][DBLP ] Inf. Comput., 1989, v:81, n:2, pp:123-167 [Journal ] Thierry Coquand , Gérard P. Huet The Calculus of Constructions [Citation Graph (0, 0)][DBLP ] Inf. Comput., 1988, v:76, n:2/3, pp:95-120 [Journal ] Thierry Coquand , Hugo Herbelin A - Translation and Looping Combinators in Pure Type Systems. [Citation Graph (0, 0)][DBLP ] J. Funct. Program., 1994, v:4, n:1, pp:77-88 [Journal ] Gilles Barthe , Thierry Coquand Remarks on the equational theory of non-normalizing pure type systems. [Citation Graph (0, 0)][DBLP ] J. Funct. Program., 2006, v:16, n:2, pp:137-155 [Journal ] Thierry Coquand , Gérard P. Huet A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 1985, v:1, n:3, pp:323-328 [Journal ] Stefano Berardi , Marc Bezem , Thierry Coquand On the Computational Content of the Axiom of Choice. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1998, v:63, n:2, pp:600-622 [Journal ] Thierry Coquand An Intuitionistic Proof of Tychonoff's Theorem. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1992, v:57, n:1, pp:28-32 [Journal ] Thierry Coquand A Semantics of Evidence for Classical Arithmetic. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1995, v:60, n:1, pp:325-337 [Journal ] Thierry Coquand Minimal Invariant Spaces in Formal Topology. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1997, v:62, n:3, pp:689-698 [Journal ] Thierry Coquand , Sara Sadocco , Giovanni Sambin , Jan M. Smith Formal Topologies on The Set of First-Order Formulae. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 2000, v:65, n:3, pp:1183-1192 [Journal ] Thierry Coquand , Bas Spitters Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. [Citation Graph (0, 0)][DBLP ] J. UCS, 2005, v:11, n:12, pp:1932-1944 [Journal ] Thierry Coquand , Bas Spitters A constructive proof of the Peter-Weyl theorem. [Citation Graph (0, 0)][DBLP ] Math. Log. Q., 2005, v:51, n:4, pp:351-359 [Journal ] Thierry Coquand , Peter Dybjer Intuitionistic Model Constructions and Normalization Proofs. [Citation Graph (0, 0)][DBLP ] Mathematical Structures in Computer Science, 1997, v:7, n:1, pp:75-94 [Journal ] Thierry Coquand , Martin Hofmann A new method for establishing conservativity of classical systems over their intuitionistic version. [Citation Graph (0, 0)][DBLP ] Mathematical Structures in Computer Science, 1999, v:9, n:4, pp:323-333 [Journal ] Thierry Coquand An Algorithm for Type-Checking Dependent Types. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 1996, v:26, n:1-3, pp:167-177 [Journal ] Thierry Coquand A syntactical proof of the Marriage Lemma. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2003, v:290, n:1, pp:1107-1113 [Journal ] Thierry Coquand Categories of Embeddings. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1989, v:68, n:3, pp:221-237 [Journal ] Thierry Coquand Another Proof of the Intuitionistic Ramsey Theorem. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1993, v:115, n:1, pp:63-75 [Journal ] Thierry Coquand , Guo-Qiang Zhang A representation of stably compact spaces, and patch topology. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2003, v:305, n:1-3, pp:77-84 [Journal ] Val Tannen , Thierry Coquand Extensional Models for Polymorphism. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1988, v:59, n:, pp:85-114 [Journal ] Andreas Abel , Thierry Coquand , Peter Dybjer Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. [Citation Graph (0, 0)][DBLP ] LICS, 2007, pp:3-12 [Conf ] Thierry Coquand , Arnaud Spiwack Towards Constructive Homological Algebra in Type Theory. [Citation Graph (0, 0)][DBLP ] Calculemus/MKM, 2007, pp:40-54 [Conf ] Thierry Coquand , Arnaud Spiwack A proof of strong normalisation using domain theory [Citation Graph (0, 0)][DBLP ] CoRR, 2007, v:0, n:, pp:- [Journal ] Andreas Abel , Thierry Coquand Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. [Citation Graph (0, 0)][DBLP ] Fundam. Inform., 2007, v:77, n:4, pp:345-395 [Journal ] Thierry Coquand The Completeness of Typing for Context-Semantics. [Citation Graph (0, 0)][DBLP ] Fundam. Inform., 2007, v:77, n:4, pp:293-301 [Journal ] Forcing and Type Theory. [Citation Graph (, )][DBLP ] Constructive Mathematics and Functional Programming (Abstract). [Citation Graph (, )][DBLP ] On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. [Citation Graph (, )][DBLP ] Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. [Citation Graph (, )][DBLP ] A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. [Citation Graph (, )][DBLP ] Spectral schemes as ringed lattices. [Citation Graph (, )][DBLP ] Metric Boolean algebras and constructive measure theory. [Citation Graph (, )][DBLP ] Two applications of Boolean models. [Citation Graph (, )][DBLP ] Intuitionistic choice and classical logic. [Citation Graph (, )][DBLP ] Space of valuations. [Citation Graph (, )][DBLP ] Search in 0.013secs, Finished in 0.019secs