The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Thierry Coquand: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. 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]
  2. 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]
  3. Gilles Barthe, Thierry Coquand
    An Introduction to Dependent Type Theory. [Citation Graph (0, 0)][DBLP]
    APPSEM, 2000, pp:1-41 [Conf]
  4. Thierry Coquand
    A Logical Approach to Abstract Algebra. [Citation Graph (0, 0)][DBLP]
    CiE, 2005, pp:86-95 [Conf]
  5. Thierry Coquand, Christine Paulin
    Inductively defined types. [Citation Graph (0, 0)][DBLP]
    Conference on Computer Logic, 1988, pp:50-66 [Conf]
  6. Thierry Coquand
    Constructive Topology and Combinatorics. [Citation Graph (0, 0)][DBLP]
    Constructivity in Computer Science, 1991, pp:159-164 [Conf]
  7. Thierry Coquand, Henrik Persson
    A Proof-Theoretical Investigation of Zantema's Problem. [Citation Graph (0, 0)][DBLP]
    CSL, 1997, pp:177-188 [Conf]
  8. Thierry Coquand, Guo-Qiang Zhang
    Sequents, Frames, and Completeness. [Citation Graph (0, 0)][DBLP]
    CSL, 2000, pp:277-291 [Conf]
  9. 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]
  10. 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]
  11. Thierry Coquand
    05021 Executive Summary -- Mathematics, Algorithms, Proofs. [Citation Graph (0, 0)][DBLP]
    Mathematics, Algorithms, Proofs, 2005, pp:- [Conf]
  12. 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]
  13. Thierry Coquand, Henri Lombardi, Peter Schuster
    A Nilregular Element Property. [Citation Graph (0, 0)][DBLP]
    Mathematics, Algorithms, Proofs, 2005, pp:- [Conf]
  14. 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]
  15. 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]
  16. Thierry Coquand, Peter Dybjer
    Inductive Definitions and Type Theory: an Introduction (Preliminary Version). [Citation Graph (0, 0)][DBLP]
    FSTTCS, 1994, pp:60-76 [Conf]
  17. Stefano Berardi, Thierry Coquand, Susumu Hayashi
    Games with 1-backtracking. [Citation Graph (0, 0)][DBLP]
    GALOP, 2005, pp:210-225 [Conf]
  18. Thierry Coquand
    An Analysis of Girard's Paradox [Citation Graph (0, 0)][DBLP]
    LICS, 1986, pp:227-236 [Conf]
  19. Thierry Coquand
    Categories of Embeddings [Citation Graph (0, 0)][DBLP]
    LICS, 1988, pp:256-263 [Conf]
  20. Thierry Coquand, Arnaud Spiwack
    A Proof of Strong Normalisation using Domain Theory. [Citation Graph (0, 0)][DBLP]
    LICS, 2006, pp:307-316 [Conf]
  21. 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]
  22. 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]
  23. Marc Bezem, Thierry Coquand
    Automating Coherent Logic. [Citation Graph (0, 0)][DBLP]
    LPAR, 2005, pp:246-260 [Conf]
  24. 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]
  25. Thierry Coquand
    Program Construction in Intuitionistic Type Theory (Abstract). [Citation Graph (0, 0)][DBLP]
    MPC, 1995, pp:49- [Conf]
  26. Thierry Coquand
    Dynamical Method in Algebra: A Survey. [Citation Graph (0, 0)][DBLP]
    TABLEAUX, 2003, pp:2- [Conf]
  27. Val Tannen, Thierry Coquand
    Extensional Models for Polymorphism. [Citation Graph (0, 0)][DBLP]
    TAPSOFT, Vol.2, 1987, pp:291-307 [Conf]
  28. 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]
  29. Thorsten Altenkirch, Thierry Coquand
    A Finitary Subsystem of the Polymorphic lambda-Calculus. [Citation Graph (0, 0)][DBLP]
    TLCA, 2001, pp:22-28 [Conf]
  30. 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]
  31. Thierry Coquand
    Completeness Theorems and lambda-Calculus. [Citation Graph (0, 0)][DBLP]
    TLCA, 2005, pp:1-9 [Conf]
  32. Thierry Coquand, Randy Pollack, Makoto Takeyama
    A Logical Framework with Dependently Typed Records. [Citation Graph (0, 0)][DBLP]
    TLCA, 2003, pp:105-119 [Conf]
  33. Thierry Coquand
    Alfa/Agda. [Citation Graph (0, 0)][DBLP]
    The Seventeen Provers of the World, 2006, pp:50-54 [Conf]
  34. Ana Bove, Thierry Coquand
    Formalising Bitonic Sort in Type Theory. [Citation Graph (0, 0)][DBLP]
    TYPES, 2004, pp:82-97 [Conf]
  35. Thierry Coquand
    Infinite Objects in Type Theory. [Citation Graph (0, 0)][DBLP]
    TYPES, 1993, pp:62-78 [Conf]
  36. Thierry Coquand, Henrik Persson
    Gröbner Bases in Type Theory. [Citation Graph (0, 0)][DBLP]
    TYPES, 1998, pp:33-46 [Conf]
  37. Thierry Coquand, Jan M. Smith
    An Application of Constructive Completeness. [Citation Graph (0, 0)][DBLP]
    TYPES, 1995, pp:76-84 [Conf]
  38. Thierry Coquand, Makoto Takeyama
    An Implementation of Type: Type. [Citation Graph (0, 0)][DBLP]
    TYPES, 2000, pp:53-62 [Conf]
  39. 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]
  40. 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]
  41. 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]
  42. 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]
  43. Thierry Coquand
    The Paradox of Trees in Type Theory. [Citation Graph (0, 0)][DBLP]
    BIT, 1992, v:32, n:1, pp:10-14 [Journal]
  44. 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]
  45. 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]
  46. 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]
  47. 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]
  48. Thierry Coquand
    An Analysis of Ramsey's Theorem [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 1994, v:110, n:2, pp:297-304 [Journal]
  49. 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]
  50. 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]
  51. 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]
  52. 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]
  53. 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]
  54. 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]
  55. 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]
  56. 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]
  57. 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]
  58. 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]
  59. 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]
  60. 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]
  61. 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]
  62. 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]
  63. 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]
  64. 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]
  65. Thierry Coquand
    Categories of Embeddings. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 1989, v:68, n:3, pp:221-237 [Journal]
  66. 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]
  67. 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]
  68. Val Tannen, Thierry Coquand
    Extensional Models for Polymorphism. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 1988, v:59, n:, pp:85-114 [Journal]
  69. 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]
  70. Thierry Coquand, Arnaud Spiwack
    Towards Constructive Homological Algebra in Type Theory. [Citation Graph (0, 0)][DBLP]
    Calculemus/MKM, 2007, pp:40-54 [Conf]
  71. Thierry Coquand, Arnaud Spiwack
    A proof of strong normalisation using domain theory [Citation Graph (0, 0)][DBLP]
    CoRR, 2007, v:0, n:, pp:- [Journal]
  72. 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]
  73. 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]

  74. Forcing and Type Theory. [Citation Graph (, )][DBLP]


  75. Constructive Mathematics and Functional Programming (Abstract). [Citation Graph (, )][DBLP]


  76. On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. [Citation Graph (, )][DBLP]


  77. Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. [Citation Graph (, )][DBLP]


  78. A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. [Citation Graph (, )][DBLP]


  79. Spectral schemes as ringed lattices. [Citation Graph (, )][DBLP]


  80. Metric Boolean algebras and constructive measure theory. [Citation Graph (, )][DBLP]


  81. Two applications of Boolean models. [Citation Graph (, )][DBLP]


  82. Intuitionistic choice and classical logic. [Citation Graph (, )][DBLP]


  83. Space of valuations. [Citation Graph (, )][DBLP]


Search in 0.208secs, Finished in 0.213secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002