Thierry Coquand

• An Introduction to Lorenzen's 'Algebraic and Logistic Investigations on Free Lattices' (1951)

  Thierry Coquand, Henri Lombardi, Stefan Neuwirth
  HISTORY AND PHILOSOPHY OF LOGIC - 2025
• A foundation for synthetic algebraic geometry

  Felix Cherubini, Thierry Coquand, Matthias Hutzler
  MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE - 2024
• A Variation of Reynolds-Hurkens Paradox

  Thierry Coquand
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) - 2024
• Constructive theory of ordinals

  Thierry Coquand, Henri Lombardi, Stefan Neuwirth
  Mathematics For Computation (M4c) - 2023
• Type Theory with Explicit Universe Polymorphism

  Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
  Leibniz International Proceedings in Informatics, LIPIcs - 2023
• REDUCTION FREE NORMALIZATION FOR A PROOF-IRRELEVANT TYPE OF PROPOSITIONS

  Thierry Coquand
  Logical Methods in Computer Science - 2023
• CANONICITY AND HOMOTOPY CANONICITY FOR CUBICAL TYPE THEORY

  Thierry Coquand, Simon Huber, C. Sattler
  Logical Methods in Computer Science - 2022
• Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism

  M. Bezem, Thierry Coquand
  Theoretical Computer Science - 2022
• Syntax and models of Cartesian cubical type theory

  C. Angiuli, G. Brunerie, Thierry Coquand, R. Harper, K. B. Hou, D. R. Licata
  Mathematical Structures in Computer Science - 2021
• Constructive sheaf models of type theory

  Thierry Coquand, Fabian Ruch, Christian Sattler
  Mathematical Structures in Computer Science - 2021
• On generalized algebraic theories and categories with families

  M. Bezem, Thierry Coquand, P. Dybjer, M. Escardo
  Mathematical Structures in Computer Science - 2021
• Formal Topology and Univalent Foundations

  Thierry Coquand, A. Tosun
  Proof and Computation II - 2021
• Regular Entailment Relations

  Thierry Coquand, Henri Lombardi, Stefan Neuwirth
  Paul Lorenzen -- Mathematician and Logician. Logic, Epistemology, and the Unity of Science. Gerhard Heinzmann, Gereon Wolters (red.) - 2021
• Lorenzen and constructive mathematics

  Thierry Coquand
  Paul Lorenzen -- Mathematician and Logician. Logic, Epistemology, and the Unity of Science. Gerhard HeinzmannGereon Wolters (red.) - 2021
• Lorenzen's Proof of Consistency for Elementary Number Theory

  Thierry Coquand, S. Neuwirth
  History and Philosophy of Logic - 2020
• FAILURE OF NORMALIZATION IN IMPREDICATIVE TYPE THEORY WITH PROOF-IRRELEVANT PROPOSITIONAL EQUALITY

  Andreas Abel, Thierry Coquand
  Logical Methods in Computer Science - 2020
• Lattice-ordered groups generated by an ordered group and regular systems of ideals

  Thierry Coquand, H. Lombardi, S. Neuwirth
  Rocky Mountain Journal of Mathematics - 2019
• Skolem's Theorem in Coherent Logic

  M. Bezem, Thierry Coquand
  Fundamenta Informaticae - 2019
• An Adequacy Theorem for Dependent Type Theory

  Thierry Coquand, Simon Huber
  Theory of Computing Systems - 2019
• The Univalence Axiom in Cubical Sets

  M. Bezem, Thierry Coquand, Simon Huber
  Journal of Automated Reasoning - 2019
• Syntactic forcing models for coherent logic

  M. Bezem, U. Buchholtz, Thierry Coquand
  Indagationes Mathematicae-New Series - 2018
• Combinatorial topology and constructive mathematics

  Thierry Coquand
  Indagationes Mathematicae-New Series - 2018
• Type Theory with Weak J

  Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, Simon Huber, Nicolai Kraus
  23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29 May - 1 June 2017, Abstracts - 2017
• THE INDEPENDENCE OF MARKOV'S PRINCIPLE IN TYPE THEORY

  Thierry Coquand, B. Mannaa
  Logical Methods in Computer Science - 2017
• Type Theory and Formalisation of Mathematics

  Thierry Coquand
  Lecture Notes in Computer Science - 2017
• Cubical type theory: a constructive interpretation of the univalence axiom

  Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
  Journal of Applied Logics - 2017
• RING DIVIDERS AND KRULL RINGS (A CONSTRUCTIVE APPROACH)

  Thierry Coquand, H. Lombardi
  Communications in Algebra - 2016
• On Decidability of Conversion in Type Theory

  Andreas Abel, Thierry Coquand, Bassel Mannaa
  22nd International Conference on Types for Proofs and Programs (TYPES 2016) - 2016
• A presheaf model of parametric type theory

  Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
  2015
• A Kripke model for simplicial sets

  M. Bezem, Thierry Coquand
  Theoretical Computer Science - 2015
• Théorie des types dépendants et axiome d'univalence

  Thierry Coquand
  Asterisque - 2015
• A Presheaf Model of Parametric Type Theory

  Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
  Electronical Notes in Theoretical Computer Science - 2015
• A generalization of the Takeuti-Gandy interpretation

  B. Barras, Thierry Coquand, Simon Huber
  Mathematical Structures in Computer Science - 2015
• Recursive Functions and Constructive Mathematics

  Thierry Coquand
  CONSTRUCTIVITY AND COMPUTABILITY IN HISTORICAL AND PHILOSOPHICAL PERSPECTIVE - 2014
• A Sheaf Model of the Algebraic Closure

  Bassel Mannaa, Thierry Coquand
  Proceedings Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, July 13, 2014, EPTCS - 2014
• Revisiting Zariski Main Theorem from a constructive point of view

  M. E. Alonso, Thierry Coquand, H. Lombardi
  Journal of Algebra - 2014
• About Goodman's Theorem

  Thierry Coquand
  Annals of Pure and Applied Logic - 2013
• Dynamic Newton-Puiseux theorem

  Bassel Mannaa, Thierry Coquand
  Journal of Logic and Analysis - 2013
• Isomorphism is equality

  Thierry Coquand, Nils Anders Danielsson
  Indagationes mathematicae - 2013
• Computing persistent homology within Coq/SSReflect

  Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
  ACM Transactions on Computational Logic - 2013
• A constructive version of Laplace's proof on the existence of complex roots

  Cyril Cohen, Thierry Coquand
  Journal of Algebra - 2013
• Constructive Finite Free Resolutions

  Thierry Coquand, Claude Quitte
  Manuscripta Mathematica - 2012
• A Formal Proof of the Sasaki-Murao Algorithm

  Thierry Coquand, Anders Mörtberg, Vincent Siles
  Journal of Formalized Reasoning - 2012
• Coherent and Strongly Discrete Rings in Type Theory

  Anders Mörtberg, Thierry Coquand, Vincent Siles
  CPP 2012, LNCS - 2012
• A modular type-checking algorithm for type theory with singleton types

  Miguel Pagano, Andreas Abel, Thierry Coquand
  Logical Methods in Computer Science - 2011
• Metric complements of overt closed sets

  Thierry Coquand, E. Palmgren, B. Spitters
  Mathematical Logic Quarterly - 2011
• A MODULAR TYPE-CHECKING ALGORITHM FOR TYPE THEORY WITH SINGLETON TYPES AND PROOF IRRELEVANCE

  A Abel, Thierry Coquand, M Pagano
  LOGICAL METHODS IN COMPUTER SCIENCE - 2011
• A Decision Procedure for Regular Expression Equivalence in Type Theory

  Thierry Coquand, Vincent Siles
  Certified Programs and Proofs : First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / edited by Jean-Pierre Jouannaud, Zhong Shao - 2011
• Unique path as formal points

  Thierry Coquand, Peter Schuster
  Journal of Logic and Analysis - 2011
• Games with 1-backtracking

  S. Berardi, Thierry Coquand, S. Hayashi
  Annals of Pure and Applied Logic - 2010

Fler publikationer

Antalet publikationer som visas på denna sida är begränsat. Besök Göteborgs Universitets publikationsdatabas (GUP) för att söka efter fler publikationer.