Thierry Coquand - Publication list since 2002#

• with E. Palmgren Constructive metric completion of Boolean algebra. Arch. Math. Logic 41 (2002), no. 7, 687-704
• A syntactical proof of the marriage lemma. Theoret. Comput. Sci. 290 (2003), no. 1, 1107-1113.
• with G.Q. Zhang. A representation of stably compact spaces, and patch topology, Theoret. Comput. Sci. 305, 2003, 77-84
• with M. Bezem. Newman's lemma|a case study in proof automation and geometric logic, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS No. 79, 2003, 86-100
• Compact spaces and distributive lattices, J. Pure Appl. Algebra 184, 2003, 86-100
• with G. Sambin, J. Smith, and S. Valentini. Inductively generated formal topology. Ann. Pure Appl. Logic 124 (2003), no. 1-3, 71-106
• with G. Barthe Remarks on the equational theory of non-normalizing pure type systems Journal of Functional Programming 14 (2004), 191-210
• Sur un théorème de Kronecker concernant les variétés algébriques C. R. Acad. Sci. Paris, Ser. I 338 (2004),291-294
• with H. Lombardi and C. Quitte. Generating non Noetherian Modules constructively Manuscripta Math. 115 (2004), no. 4, 513-520
• About Stone's notion of spectrum J. Pure Appl. Algebra, 2005
• A note on measures with values in partially ordered vector space. Positivity, 2004
• with H. Lombardi. A short proof for the Krull dimension of a polynomial ring. Amer. Math. Monthly 112 (2005), no. 9, 826-829
• with H. Lombardi and P. Schuster. A nilregular element property. Arch. Math. (Basel), 85 pp. 49-54
• with B. Spitters A constructive proof of the Peter-Weyl theorem. MLQ Math. Log. Q., 51 pp. 351-359
• with B. Spitters Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems Journal of Universal computation volume 11, issue 12 2005
• Geometric Hahn-Banach. Math. Proc. Cambridge Philos. Soc. 2006
• On Seminormality. J. Algebra 305 (2006), no. 1, 577-584
• with H. Lombardi A logical approach to abstract algebra. Math. Structures Comput. Sci. 16 (2006), no. 5, 885-900
• with A. Spiwack Strong Normalisation with Domain Theory, to appear in Logical Methods in Computer Science, selected issue from LICS 2006
• with H. Lombardi and P. Schuster. The projective spectrum as a distributive lattice. Cahiers de Topologie et Géométrie différentielles catégoriques. (2007)
• The completness of typing for context-semantics. Fundamenta Informatica (2007), selected issue from TLCA 2005
• with A. Spiwack. A proof of strong normalisation using domain theory. Logical Method in Computer Science 3 (4) 2007
• A Space of Valuations. Ann. Pure Appl. Logic 157 (2009), no. 2-3, 97-109
• with B. Spitters. Constructive Gelfand duality for C* algebras. Math. Proc. Cambridge Philos. Soc. 147 (2009), no. 2, 339-344
• with B. Spitters. Integrals and valuations. J. Log. Anal. 1 (2009), Paper 3, 22 pp.
• with L. Ducos,H. Lombardi,C. Quitté. Constructive Krull dimension. I. Integral extensions. J. Algebra Appl. 8 (2009), no. 1, 129-138
• with H. Lombardi and P. Schuster. Spectral schemes as ringed lattices. Ann. Math. Artif. Intell., 2009
• with G. Jaber. A note on forcing and type theory. Fundamenta Informatica, 2010
• with H. Lombardi and C. Quitté. Curves and coherent Prüfer rings. Journal of Symbolic Computations, December 2010
• with B. Spitters, Constructive Theory of Banach algebras, Journal of Logic and Analysis, to appear
• with E. Palmgren and B. Spitters, Metric complement of overt closed sets. Mathematical Logic Quaterly, to appear

• with R. Pollack and M. Takayema A Logical Framework with Dependently Typed Records. Typed Lambda Calculus and Applications'03
• with H. Lombardi. Hidden constructions in abstract algebra (3) Krull dimension of distributive lattices and commutative rings. in: Commutative ring theory and applications. Eds: Fontana M., Kabbaj S.-E., Wiegand S. Lecture notes in pure and applied mathematics vol 131. (2002) pp. 477-499.
• with A. Bove. Formalising Bitonic Sort in Type Theory. Types for Proofs and Programs TYPES 2004, LNCS 3839 pp. 83-98.
• with H. Lombardi A Logical Approach to Abstract Algebra. CiE2005, pp. 86-95.
• with M. Bezem. Automating Coherent Logic. LPAR 2005, pp. 246-260.
• with A. Abel and U. Norell. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.
• with A. Abel. Untyped Algorithmic Equality for Martin-Lf's Logical Framework with Surjective Pairs. TLCA 2005, pp. 23-38
• with A. Spiwack. Strong Normalisation with Domain Theory. LICS 2006.
• with A. Spiwack Towards constructive homological algebra in Type Theory. Calculemus 2007.
• with A. Abel and P. Dybjer Dependent Types with Universes via Normalization-by-Evaluation LICS 2007.
• with A. Abel and M. Pagano. Type-checking dependent types TLCA 2009.

• A completness theorem for geometrical logic Invited Talk, Logic, Philosophy and Methodology of Science, 2003, to appear, 2004
• Completeness Theorems and lambda-Calculus. Invited talk, TLCA 2005, pp. 1-9

• La contribution de Kolmogorov en logique intuitionniste. (sous la direction de Éric Charpentier et Nikolai Nikolski), collection Échelles, 2005. Has been translated for an English edition 2007.
• with H. Lombardi and M.F. Roy An elementary characterization of Krull dimension. in From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics. (L. Crosilla, P. Schuster, eds.). Oxford University Press, pp. 239-244.

• Entry on Type Theory in the Stanford Encyclopedia of Philosophy see
• T. Coquand, P. Dybjer, E. Palmgren. Type-theoretic Foundations of Constructive Mathematics. Draft (171 pages) conditionally accepted for publication by Cambridge University Press.

• with G.Huet The calculus of constructions. Information and Computation, 1988.
• with Ch. Paulin-Mohring Inductively defined types. LNCS 417, COLOG-88.
• Constructions: A higher order proof system for mechanizing mathematics, LNCS, Proceeding of Eurocal 1985.
• Pattern-Matching with dependent types. Proceedings of the Workshop on Types for Proofs and Programs, 1992.
• An analysis of Girard's paradox, LICS 1986.
• Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science. Academic Press, 1990.
• A semantics of evidence for classical logic. Journal of Symbolic Logic, 1995.

• An analysis of Girard's paradox, LICS 1986.
• with A. Spiwack. A proof of strong normalisation using domain theory. Logical Method in Computer Science 3 (4) 2007
• Sur un théorème de Kronecker concernant les variétés algébriques C. R. Acad. Sci. Paris, Ser. I 338 (2004),291-294
• with H. Lombardi and C. Quitte. Generating non Noetherian Modules constructively Manuscripta Math. 115 (2004), no. 4, 513-520.