Thierry Coquand
-
FAILURE OF NORMALIZATION IN IMPREDICATIVE TYPE THEORY WITH PROOF-IRRELEVANT PROPOSITIONAL
EQUALITY
Andreas Abel, Thierry Coquand
Logical Methods in Computer Science - 2020-01-01 -
Lorenzen's Proof of Consistency for Elementary Number
Theory
Thierry Coquand, S. Neuwirth
History and Philosophy of Logic - 2020-01-01 -
Skolem's Theorem in Coherent
Logic
M. Bezem, Thierry Coquand
Fundamenta Informaticae - 2019-01-01 -
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-01-01 -
An Adequacy Theorem for Dependent Type
Theory
Thierry Coquand, Simon Huber
Theory of Computing Systems - 2019-01-01 -
The Univalence Axiom in Cubical
Sets
M. Bezem, Thierry Coquand, Simon Huber
Journal of Automated Reasoning - 2019-01-01 -
Combinatorial topology and constructive
mathematics
Thierry Coquand
Indagationes Mathematicae-New Series - 2018-01-01 -
Syntactic forcing models for coherent
logic
M. Bezem, U. Buchholtz, Thierry Coquand
Indagationes Mathematicae-New Series - 2018-01-01 -
Cubical type theory: a constructive interpretation of the univalence
axiom
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Journal of Applied Logics - 2017-01-01 -
Type Theory and Formalisation of
Mathematics
Thierry Coquand
Lecture Notes in Computer Science - 2017-01-01 -
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-01-01 -
THE INDEPENDENCE OF MARKOV'S PRINCIPLE IN TYPE
THEORY
Thierry Coquand, B. Mannaa
Logical Methods in Computer Science - 2017-01-01 -
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-01-01 -
RING DIVIDERS AND KRULL RINGS (A CONSTRUCTIVE
APPROACH)
Thierry Coquand, H. Lombardi
Communications in Algebra - 2016-01-01 -
A presheaf model of parametric type
theory
Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
- 2015-01-01 -
A Kripke model for simplicial
sets
M. Bezem, Thierry Coquand
Theoretical Computer Science - 2015-01-01 -
Théorie des types dépendants et axiome
d'univalence
Thierry Coquand
Asterisque - 2015-01-01 -
A Presheaf Model of Parametric Type
Theory
Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin
Electronical Notes in Theoretical Computer Science - 2015-01-01 -
A generalization of the Takeuti-Gandy
interpretation
B. Barras, Thierry Coquand, Simon Huber
Mathematical Structures in Computer Science - 2015-01-01 -
Recursive Functions and Constructive
Mathematics
Thierry Coquand
CONSTRUCTIVITY AND COMPUTABILITY IN HISTORICAL AND PHILOSOPHICAL PERSPECTIVE - 2014-01-01 -
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-01-01 -
Revisiting Zariski Main Theorem from a constructive point of
view
M. E. Alonso, Thierry Coquand, H. Lombardi
Journal of Algebra - 2014-01-01 -
About Goodman's
Theorem
Thierry Coquand
Annals of Pure and Applied Logic - 2013-01-01 -
Dynamic Newton-Puiseux
theorem
Bassel Mannaa, Thierry Coquand
Journal of Logic and Analysis - 2013-01-01 -
Isomorphism is
equality
Thierry Coquand, Nils Anders Danielsson
Indagationes mathematicae - 2013-01-01 -
Computing persistent homology within
Coq/SSReflect
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
ACM Transactions on Computational Logic - 2013-01-01 -
A constructive version of Laplace's proof on the existence of complex
roots
Cyril Cohen, Thierry Coquand
Journal of Algebra - 2013-01-01 -
Constructive Finite Free
Resolutions
Thierry Coquand, Claude Quitte
Manuscripta Mathematica - 2012-01-01 -
A Formal Proof of the Sasaki-Murao
Algorithm
Thierry Coquand, Anders Mörtberg, Vincent Siles
Journal of Formalized Reasoning - 2012-01-01 -
Coherent and Strongly Discrete Rings in Type
Theory
Anders Mörtberg, Thierry Coquand, Vincent Siles
CPP 2012, LNCS - 2012-01-01 -
A modular type-checking algorithm for type theory with singleton
types
Miguel Pagano, Andreas Abel, Thierry Coquand
Logical Methods in Computer Science - 2011-01-01 -
Metric complements of overt closed
sets
Thierry Coquand, E. Palmgren, B. Spitters
Mathematical Logic Quarterly - 2011-01-01 -
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-01-01 -
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-01-01 -
Unique path as formal
points
Thierry Coquand, Peter Schuster
Journal of Logic and Analysis - 2011-01-01 -
Games with
1-backtracking
S. Berardi, Thierry Coquand, S. Hayashi
Annals of Pure and Applied Logic - 2010-01-01 -
Curves and coherent Prufer
rings
Thierry Coquand, Henri Lombardi, Claude Quitte
JOURNAL OF SYMBOLIC COMPUTATION - 2010-01-01 -
A Note on Forcing and Type
Theory
Thierry Coquand, Guilhem Jaber
FUNDAMENTA INFORMATICAE - 2010-01-01 -
Constructive Gelfand duality for
C*-algebras
Thierry Coquand, Bas Spitters
Mathematical Proceedings of the Cambridge Philosophical Society - 2009-01-01 -
A simple type-theoretic language:
Mini-TT
Thierry Coquand, Y. Kinoshita, Bengt Nordström, M. Takeyama
From Semantics to Computer Science : Essays in Honour of Gilles Kahn - 2009-01-01 -
Spectral schemes as ringed
lattices
Thierry Coquand, Henri Lombardi, Peter Schuster
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE - 2009-01-01 -
Constructive Krull Dimension. I: Integral
Extensions
Thierry Coquand, Lionel Ducos, Henri Lombardi, Claude Quitte
JOURNAL OF ALGEBRA AND ITS APPLICATIONS - 2009-01-01 -
Space of
Valuations
Thierry Coquand
Annals of Pure and Applied Logic - 2009-01-01 -
Integrals and
Valuations
Thierry Coquand, Bas Spitters
Logic and Analysis - 2009-01-01 -
forcing in type
theory
Thierry Coquand
Proceeding of CSL 09 - 2009-01-01 -
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof
Irrelevance
Thierry Coquand
TLCA 2009 - 2009-01-01 -
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type
Theory
Andreas Abel, Thierry Coquand, Peter Dybjer
FLOPS 2008 - 2008-01-01 -
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type
Theory
Andreas Abel, Thierry Coquand, Peter Dybjer
Mathematics of Program Construction 2008 - 2008-01-01 -
A note on the axiomatisation of real
numbers
Thierry Coquand
Math.Log. Q. - 2008-01-01 -
Normalization by Evaluation for Martin-Löf Type Theory with Equality
Judgements
Andreas Abel, Thierry Coquand, Peter Dybjer
Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007. - 2007-01-01 -
Untyped algorithmic equality for Martin-Löf's logical framework with surjective
pairs
Andreas Abel, Thierry Coquand
Fundamenta Informaticae - 2007-01-01 -
Towards constructive homological algebra in type
theory
Thierry Coquand, Arnaud Spiwack
Proceeding of Calculemus 2007 - 2007-01-01 -
The completeness of typing for
context-semantics
Thierry Coquand
Fundamenta Informaticae - 2007-01-01 -
Remarks on the equational theory of non-normalizing pure type
systems
G. Barthe, Thierry Coquand
Journal of Functional Programming - 2006-01-01 -
Geometric Hahn-Banach
theorem
Thierry Coquand
Math. Proc. Cambridge Philos. Soc - 2006-01-01 -
Preface of special issue on formal
topology
Thierry Coquand, Giovanni Sambin
Annals of Pure and Applied Logic - 2006-01-01 -
A logical approach to abstract
algebra
Thierry Coquand, Henri Lombardi
Mathematical Structures in Computer Science - 2006-01-01 -
On
seminormality
Thierry Coquand
Journal of Algebra - 2006-01-01 -
A Proof of Strong Normalisation Using Domain
Theory
Thierry Coquand, Arnaud Spiwack
proceeding of Logic in Computer Science, 2006 - 2006-01-01 -
Connecting a Logical Framework to a First-Order Logic
Prover.
Thierry Coquand, Andreas Abel, Ulf Norell
FroCos 2005 - 2005-01-01 -
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective
Pairs.
Thierry Coquand, Andreas Abel
Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005); in: LECTURE NOTES IN COMPUTER SCIENCE , Volume: 3461) - 2005-01-01 -
A nilregular element
property.
Thierry Coquand, Henri Lombardi, Peter Schuster
Arch. Math. (Basel) - 2005-01-01 -
About Stone Notion of
Spectrum
Thierry Coquand
Journal of Pure and Applied Algebra - 2005-01-01 -
Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation
theorems.
Thierry Coquand, Bas Spiiters
J.UCS 11 - 2005-01-01 -
Automating Coherent
Logic.
Thierry Coquand, Marc Bezem
LPAR 2005 - 2005-01-01 -
A Logical Framework with Dependently Typed
Records.
Thierry Coquand, Makoto Takeyama, Randy Pollack
Fundam. Inform. - 2005-01-01 -
A Logical Approach to Abstract
Algebra.
Thierry Coquand
CiE2005 - 2005-01-01 -
Completeness Theorems and
lambda-Calculus.
Thierry Coquand
TLCA 2005 - 2005-01-01 -
A constructive proof of the Peter-Weyl
theorem
Thierry Coquand, Bas Spitters
MLQ Math. Log. Q. - 2005-01-01 -
A Completeness Proof for Geometrical
Logic
Thierry Coquand
Logic, Methodology and Philosophy of Sciences. Preceedings of the Twelfth International Congress. Hajek, Valdes-Villuaneva, Westerstahl, editors - 2005-01-01 -
An elementary characterization of Krull
dimension
Thierry Coquand, Henri Lombardi, Marie-Francoise Roy
From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics. (L. Crosilla, P. Schuster, eds.). Oxford University Press, - 2005-01-01 -
Formalising Bitonic Sort in Type
Theory
Ana Bove, Thierry Coquand
Types for Proofs and Programs TYPES 2004 - 2005-01-01 -
Sur un théorème de Kronecker concernant les variétés
algébriques
Thierry Coquand
Comptes rendus. Mathematique - 2004-01-01 -
Generating non noetherian modules
constructively
Thierry Coquand, H. Lombardi, C. Quitte
Manuscripta mathematica - 2004-01-01 -
Proof-theoretical analysis of order
relations
S. Negri, J. von Plato, Thierry Coquand
Archive for mathematical logic - 2004-01-01 -
La contribution de Kolmogoroven logique
intuitioniste
Thierry Coquand
L'héritage de Kolmogorov en mathématiques - 2004-01-01 -
Generating non-Noetherian modules
constructively
Thierry Coquand, Henri Lombardi, Claude Quitte
Manuscripta Math - 2004-01-01 -
On a theorem of Kronecker about algebraic
sets
Thierry Coquand
C. R. Math. Acad. Sci. Paris - 2004-01-01 -
A note on measures with values in a partially ordered vector
space.
Thierry Coquand
Positivity - 2004-01-01 -
Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative
rings
Thierry Coquand, Henri Lombardi
Commutative ring theory and applications. 4th International Conference on Commutative Algebra, Fez, 2001 - 2003-01-01 -
Inductively generated formal
topologies
Thierry Coquand, G. Sambin, Jan Smith, S. Valentini
Annals of Pure and Applied Logic - 2003-01-01 -
Compact spaces and distributive
lattices
Thierry Coquand
Journal of Pure and Applied Algebra - 2003-01-01 -
A syntactical proof of the marriage
lemma
Thierry Coquand
Theoretical Computer Science - 2003-01-01 -
A Logical Framework with Dependently Typed
Records
Thierry Coquand, R. Pollack, Makoto Takeyama
Lecture Notes in Computer Science. 6th International Conference on Typed Lambda Calculi and Applications (TLCA 2003), Valencia, 10-12 June 2003 - 2003-01-01 -
Newman's lemma - a case study in proof automation and geometric
logic
Marc Bezem, Thierry Coquand
European Association for Theoretical Computer Science. Bulletin - 2003-01-01 -
Types for Proofs and Programs - nternational Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers (Lecture Notes in Computer Science, Vol.
1956)
Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan Smith
- 2000-01-01 -
Intuitionistic choice and classical
logic
Thierry Coquand, Erik Palmgren
- 1997-01-01 -
Intuitionistic model constructions and normalization
proofs
Peter Dybjer, Thierry Coquand
Mathematical Structures in Computer Science - 1997-01-01 -
Inductive definitions and type theory an introduction (preliminary
version)
Peter Dybjer, Thierry Coquand
Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India; (Lecture Notes in Computer Science; 880) - 1994-01-01 -
Intuitionistic model constructions and normalization
proofs
Peter Dybjer, Thierry Coquand
Proceedings of the 1993 TYPES Workshop, Nijmegen - 1993-01-01