Cohen, Cyril; Coquand, Thierry: A constructive version of Laplace's proof on the existence of complex roots. Journal of Algebra, 381 (1) pp. 110-115.

Coquand, Thierry: About Goodman's Theorem. Annals of Pure and Applied Logic, 164 (4) pp. 437-442.

Mörtberg, Anders; Coquand, Thierry; Siles, Vincent: Coherent and Strongly Discrete Rings in Type Theory. CPP 2012, LNCS , 7679 pp. 273-288.

Abel, A; Coquand, Thierry; Pagano, M: A MODULAR TYPE-CHECKING ALGORITHM FOR TYPE THEORY WITH SINGLETON TYPES AND PROOF IRRELEVANCE. LOGICAL METHODS IN COMPUTER SCIENCE, 7 (2)

Coquand, Thierry; Siles, Vincent: A Decision Procedure for Regular Expression Equivalence in Type Theory. Certified Programs and Proofs : First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / edited by Jean-Pierre Jouannaud, Zhong Shao, 7086 pp. 119-134. ISBN/ISSN: 978-3-642-25379-9

Coquand, Thierry; Quitte, Claude: Constructive Finite Free Resolutions. Manuscripta Mathematica, 137 pp. 331-345.

Coquand, Thierry; Palmgren, E.; Spitters, B.: Metric complements of overt closed sets. Mathematical Logic Quarterly, 57 (4) pp. 373-378.

Coquand, Thierry; Schuster, Peter: Unique path as formal points. Journal of Logic and Analysis, 3

Pagano, Miguel; Abel, Andreas; Coquand, Thierry: A modular type-checking algorithm for type theory with singleton types. Logical Methods in Computer Science, 7

Berardi, S.; Coquand, Thierry; Hayashi, S.: Games with 1-backtracking. Annals of Pure and Applied Logic, 161 (10) pp. 1254-1269.

Coquand, Thierry; Jaber, Guilhem: A Note on Forcing and Type Theory. FUNDAMENTA INFORMATICAE, 100 (1-4) pp. 43-52.

Coquand, Thierry; Lombardi, Henri; Quitte, Claude: Curves and coherent Prufer rings. JOURNAL OF SYMBOLIC COMPUTATION, 45 (12) pp. 1378-1390.

Coquand, Thierry: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009,

Coquand, Thierry; Kinoshita, Y.; Nordström, Bengt; Takeyama, M.: A simple type-theoretic language: Mini-TT. From Semantics to Computer Science : Essays in Honour of Gilles Kahn, pp. 139-164. ISBN/ISSN: 9780521518253

Coquand, Thierry; Spitters, Bas: Constructive Gelfand duality for C*-algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 147 pp. 339-344.

Coquand, Thierry; Ducos, Lionel; Lombardi, Henri; Quitte, Claude: Constructive Krull Dimension. I: Integral Extensions. JOURNAL OF ALGEBRA AND ITS APPLICATIONS, 8 (1) pp. 129-138.

Coquand, Thierry; Spitters, Bas: Integrals and Valuations. Logic and Analysis, 1

Coquand, Thierry: Space of Valuations. Annals of Pure and Applied Logic, 157 pp. 97-109.

Coquand, Thierry; Lombardi, Henri; Schuster, Peter: Spectral schemes as ringed lattices. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 56 (3-4) pp. 339-360.

Coquand, Thierry: forcing in type theory. Proceeding of CSL 09, pp. 2.

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008, pp. 3-13.

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. Mathematics of Program Construction 2008, pp. 29-56.

Coquand, Thierry: A note on the axiomatisation of real numbers. Math.Log. Q., 54 pp. 224-228.

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements. Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.,

Abel, Andreas; Coquand, Thierry: Untyped algorithmic equality for with surjective pairs Martin-Lof's logical framework. Fundamenta Informaticae, 77 (4) pp. 345-395.

Coquand, Thierry: The completeness of typing for context-semantics. Fundamenta Informaticae, 77 (4) pp. 293-301.

Coquand, Thierry; Spiwack, Arnaud: Towards constructive homological algebra in type theory. Proceeding of Calculemus 2007,

Barthe, G.; Coquand, Thierry: Remarks on the equational theory of non-normalizing pure type systems. Journal of Functional Programming, 16 (2) pp. 137-155.

Coquand, Thierry; Spiwack, Arnaud: A Proof of Strong Normalisation Using Domain Theory. proceeding of Logic in Computer Science, 2006,

Coquand, Thierry; Lombardi, Henri: A logical approach to abstract algebra. Mathematical Structures in Computer Science, 16 (5) pp. 885-900.

Coquand, Thierry: Geometric Hahn-Banach theorem. Math. Proc. Cambridge Philos. Soc, 140 (2) pp. 313-315.

Coquand, Thierry: On seminormality. Journal of Algebra, 305 (1) pp. 577-584.

Coquand, Thierry; Sambin, Giovanni: Preface of special issue on formal topology. Annals of Pure and Applied Logic, 137 (1-3) pp. 1-2.

Bove, Ana; Coquand, Thierry: Formalising Bitonic Sort in Type Theory. Types for Proofs and Programs TYPES 2004, LNCS 3839 pp. 82-97.

Coquand, Thierry; Lombardi, Henri; Roy, Marie-Francoise: An elementary characterization of Krull dimension. 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.

Coquand, Thierry: A Completeness Proof for Geometrical Logic. Logic, Methodology and Philosophy of Sciences. Preceedings of the Twelfth International Congress. Hajek, Valdes-Villuaneva, Westerstahl, editors, pp. 79-90.

Coquand, Thierry: A Logical Approach to Abstract Algebra.. CiE2005, pp. 86-95.

Coquand, Thierry; Takeyama, Makoto; Pollack, Randy: A Logical Framework with Dependently Typed Records.. Fundam. Inform., 65 pp. 113-134.

Coquand, Thierry; Spitters, Bas: A constructive proof of the Peter-Weyl theorem. MLQ Math. Log. Q., 51 pp. 351-359.

Coquand, Thierry; Lombardi, Henri; Schuster, Peter: A nilregular element property.. Arch. Math. (Basel), 85 pp. 49-54.

Coquand, Thierry: About Stone Notion of Spectrum. Journal of Pure and Applied Algebra, 197 (1-3) pp. 141-158.

Coquand, Thierry; Bezem, Marc: Automating Coherent Logic.. LPAR 2005, pp. 246-260.

Coquand, Thierry: Completeness Theorems and lambda-Calculus.. TLCA 2005, pp. 1-9.

Coquand, Thierry; Abel, Andreas; Norell, Ulf: Connecting a Logical Framework to a First-Order Logic Prover. . FroCos 2005, pp. 285-301.

Coquand, Thierry; Spiiters, Bas: Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems.. J.UCS 11 , 11 (12) pp. 1932-1944.

Coquand, Thierry; Abel, Andreas: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. . Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005); in: LECTURE NOTES IN COMPUTER SCIENCE , Volume: 3461) , pp. 23-38.

Coquand, Thierry: A note on measures with values in a partially ordered vector space.. Positivity, 8 pp. 395-400.

Coquand, Thierry; Lombardi, Henri; Quitte, Claude: Generating non-Noetherian modules constructively. Manuscripta Math, 115 (4) pp. 513-520.

Coquand, Thierry: On a theorem of Kronecker about algebraic sets. C. R. Math. Acad. Sci. Paris, 338 (4) pp. 291-294.

Coquand, Thierry; Pollack, R.; Takeyama, Makoto: A Logical Framework with Dependently Typed Records. Lecture Notes in Computer Science. 6th International Conference on Typed Lambda Calculi and Applications (TLCA 2003), Valencia, 10-12 June 2003, 2701 pp. 105-119.

Coquand, Thierry: A syntactical proof of the marriage lemma. Theoretical Computer Science, 290 (1) pp. 1107-1113.

Coquand, Thierry: Compact spaces and distributive lattices. Journal of Pure and Applied Algebra, 184 (1) pp. 1-6.

Coquand, Thierry; Lombardi, Henri: Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. Commutative ring theory and applications. 4th International Conference on Commutative Algebra, Fez, 2001, 231 pp. 477-499. ISBN/ISSN: 0-8247-0855-5

Coquand, Thierry; Sambin, G.; Smith, Jan; Valentini, S.: Inductively generated formal topologies. Annals of Pure and Applied Logic, 124 (1-3) pp. 71–106.

Coquand, Thierry; Palmgren, Erik: Intuitionistic choice and classical logic.

Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7 pp. 75-94.

Dybjer, Peter; Coquand, Thierry: Inductive definitions and type theory an introduction. Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India, LNCS, 880

Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Proceedings of the 1993 TYPES Workshop, Nijmegen,