Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDThierry Coquand
Person information
- affiliation: University of Gothenburg, Sweden
- award (2013): ACM Software System Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2022
[j73]Thierry Coquand, Simon Huber, Christian Sattler:
Canonicity and homotopy canonicity for cubical type theory. Log. Methods Comput. Sci. 18(1) (2022)- [j72]Marc Bezem, Thierry Coquand:
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theor. Comput. Sci. 913: 1-7 (2022) - [i19]Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal:
Controlling unfolding in type theory. CoRR abs/2210.05420 (2022) - [i18]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
Type Theories with Universe Level Judgements. CoRR abs/2212.03284 (2022) - 2021
- [j71]Carlo Angiuli
, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata:
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31(4): 424-468 (2021) - [j70]Thierry Coquand, Fabian Ruch, Christian Sattler:
Constructive sheaf models of type theory. Math. Struct. Comput. Sci. 31(9): 979-1002 (2021) - [j69]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. 31(9): 1006-1023 (2021) - [i17]Thierry Coquand:
Reduction Free Normalisation for a proof irrelevant type of propositions. CoRR abs/2103.04287 (2021) - [i16]Thierry Coquand, Hajime Ishihara, Sara Negri, Peter M. Schuster:
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). Dagstuhl Reports 11(10): 151-172 (2021) - 2020
- [j68]Andreas Abel, Thierry Coquand:
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Log. Methods Comput. Sci. 16(2) (2020) - [i15]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
A Note on Generalized Algebraic Theories and Categories with Families. CoRR abs/2012.08370 (2020)
2010 – 2019
- 2019
- [j67]Marc Bezem, Thierry Coquand:
Skolem's Theorem in Coherent Logic. Fundam. Informaticae 170(1-3): 1-14 (2019) - [j66]Marc Bezem, Thierry Coquand, Simon Huber:
The Univalence Axiom in Cubical Sets. J. Autom. Reason. 63(2): 159-171 (2019) - [j65]Thierry Coquand, Maria Emilia Maietti, Erik Palmgren:
Preface to the special issue for The Fifth Workshop on Formal Topology. J. Log. Anal. 11 (2019) - [j64]Thierry Coquand, Simon Huber:
An Adequacy Theorem for Dependent Type Theory. Theory Comput. Syst. 63(4): 647-665 (2019) - [j63]Thierry Coquand:
Canonicity and normalization for dependent type theory. Theor. Comput. Sci. 777: 184-191 (2019) - [c60]Thierry Coquand, Simon Huber, Christian Sattler:
Homotopy Canonicity for Cubical Type Theory. FSCD 2019: 11:1-11:23 - [i14]Thierry Coquand, Simon Huber, Christian Sattler:
Homotopy canonicity for cubical type theory. CoRR abs/1902.06572 (2019) - [i13]Andreas Abel, Thierry Coquand:
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. CoRR abs/1911.08174 (2019) - 2018
- [j62]Thierry Coquand:
A survey of constructive presheaf models of univalence. ACM SIGLOG News 5(3): 54-65 (2018) - [c59]Thierry Coquand:
Inner Models of Univalence. LICS 2018: 11-12 - [c58]Thierry Coquand, Simon Huber, Anders Mörtberg:
On Higher Inductive Types in Cubical Type Theory. LICS 2018: 255-264 - [i12]Thierry Coquand, Simon Huber, Anders Mörtberg:
On Higher Inductive Types in Cubical Type Theory. CoRR abs/1802.01170 (2018) - [i11]Thierry Coquand:
Canonicity and normalisation for Dependent Type Theory. CoRR abs/1810.09367 (2018) - 2017
- [j61]Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch:
Notions of Anonymous Existence in Martin-Löf Type Theory. Log. Methods Comput. Sci. 13(1) (2017) - [j60]Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg:
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4(10): 3127-3170 (2017) - [j59]Thierry Coquand, Bassel Mannaa:
The Independence of Markov's Principle in Type Theory. Log. Methods Comput. Sci. 13(3) (2017) - [c57]Thierry Coquand:
Type Theory and Formalisation of Mathematics. CSR 2017: 1-6 - [c56]Thierry Coquand, Bassel Mannaa, Fabian Ruch:
Stack semantics of type theory. LICS 2017: 1-11 - [i10]Thierry Coquand, Bassel Mannaa, Fabian Ruch:
Stack Semantics of Type Theory. CoRR abs/1701.02571 (2017) - [i9]Marc Bezem, Thierry Coquand, Simon Huber:
The univalence axiom in cubical sets. CoRR abs/1710.10941 (2017) - 2016
- [j58]Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin, Peter Schuster:
Preface. Ann. Pure Appl. Log. 167(9): 725 (2016) - [c55]Thierry Coquand, Anuj Dawar:
The Ackermann Award 2016. CSL 2016: 1:1-1:4 - [c54]Thierry Coquand, Bassel Mannaa:
The Independence of Markov's Principle in Type Theory. FSCD 2016: 17:1-17:18 - [c53]Robin Adams, Marc Bezem, Thierry Coquand:
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. TYPES 2016: 3:1-3:20 - [c52]Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann:
Realizability at Work: Separating Two Constructive Notions of Finiteness. TYPES 2016: 6:1-6:23 - [i8]Thierry Coquand, Bassel Mannaa:
The Independence of Markov's Principle in Type Theory. CoRR abs/1602.04530 (2016) - [i7]Robin Adams, Marc Bezem, Thierry Coquand:
A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR abs/1610.00026 (2016) - [i6]Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg:
Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR abs/1611.02108 (2016) - 2015
- [j57]Bruno Barras, Thierry Coquand, Simon Huber:
A generalization of the Takeuti-Gandy interpretation. Math. Struct. Comput. Sci. 25(5): 1071-1099 (2015) - [j56]Marc Bezem, Thierry Coquand:
A Kripke model for simplicial sets. Theor. Comput. Sci. 574: 86-91 (2015) - [c51]Marc Bezem, Thierry Coquand, Erik Parmann:
Non-Constructivity in Kan Simplicial Sets. TLCA 2015: 92-106 - [c50]Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg:
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. TYPES 2015: 5:1-5:34 - [c49]Jean-Philippe Bernardy, Thierry Coquand, Guilhem Moulin:
A Presheaf Model of Parametric Type Theory. MFPS 2015: 67-82 - 2014
- [c48]Bassel Mannaa, Thierry Coquand:
A Sheaf Model of the Algebraic Closure. CL&C 2014: 18-32 - 2013
- [j55]Thierry Coquand:
About Goodman's Theorem. Ann. Pure Appl. Log. 164(4): 437-442 (2013) - [j54]Bassel Mannaa, Thierry Coquand:
Dynamic Newton-Puiseux theorem. J. Log. Anal. 5 (2013) - [j53]Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles:
Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14(4): 26:1-26:16 (2013) - [c47]Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch:
Generalizations of Hedberg's Theorem. TLCA 2013: 173-188 - [c46]Marc Bezem, Thierry Coquand, Simon Huber:
A Model of Type Theory in Cubical Sets. TYPES 2013: 107-128 - 2012
- [j52]Andrej Bauer, Thierry Coquand, Giovanni Sambin, Peter M. Schuster:
Preface. Ann. Pure Appl. Log. 163(2): 85-86 (2012) - [j51]Thierry Coquand, Anders Mörtberg, Vincent Siles:
A formal proof of Sasaki-Murao algorithm. J. Formaliz. Reason. 5(1): 27-36 (2012) - [j50]Thierry Coquand, Bas Spitters:
A constructive proof of Simpson's Rule. J. Log. Anal. 4 (2012) - [c45]Thierry Coquand, Anders Mörtberg, Vincent Siles:
Coherent and Strongly Discrete Rings in Type Theory. CPP 2012: 273-288 - [c44]Thierry Coquand, Anuj Dawar, Damian Niwinski:
The Ackermann Award 2012. CSL 2012: 1-5 - [c43]Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt:
Stop When You Are Almost-Full - Adventures in Constructive Termination. ITP 2012: 250-265 - [p3]Thierry Coquand, Guilhem Jaber:
A Computational Interpretation of Forcing in Type Theory. Epistemology versus Ontology 2012: 203-213 - [i5]Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles:
Computing Persistent Homology within Coq/SSReflect. CoRR abs/1209.1905 (2012) - 2011
- [j49]Andreas Abel, Thierry Coquand, Miguel Pagano:
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance. Log. Methods Comput. Sci. 7(2) (2011) - [j48]Thierry Coquand, Peter Schuster:
Unique paths as formal points. J. Log. Anal. 3 (2011) - [j47]Thierry Coquand, Erik Palmgren, Bas Spitters:
Metric complements of overt closed sets. Math. Log. Q. 57(4): 373-378 (2011) - [c42]Thierry Coquand, Vincent Siles:
A Decision Procedure for Regular Expression Equivalence in Type Theory. CPP 2011: 119-134 - 2010
- [j46]Stefano Berardi, Thierry Coquand, Susumu Hayashi:
Games with 1-backtracking. Ann. Pure Appl. Log. 161(10): 1254-1269 (2010) - [j45]Thierry Coquand, Guilhem Jaber:
A Note on Forcing and Type Theory. Fundam. Informaticae 100(1-4): 43-52 (2010) - [j44]Thierry Coquand, Bas Spitters:
Constructive theory of Banach algebras. J. Log. Anal. 2 (2010) - [j43]Thierry Coquand, Henri Lombardi, Claude Quitté:
Curves and coherent Prüfer rings. J. Symb. Comput. 45(12): 1378-1390 (2010)
2000 – 2009
- 2009
- [j42]Thierry Coquand, Henri Lombardi, Peter Schuster:
Spectral schemes as ringed lattices. Ann. Math. Artif. Intell. 56(3-4): 339-360 (2009) - [j41]Thierry Coquand:
Space of valuations. Ann. Pure Appl. Log. 157(2-3): 97-109 (2009) - [j40]Thierry Coquand, Bas Spitters:
Integrals and valuations. J. Log. Anal. 1 (2009) - [c41]Thierry Coquand:
Forcing and Type Theory. CSL 2009: 2 - [c40]Andreas Abel, Thierry Coquand, Miguel Pagano:
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. TLCA 2009: 5-19 - 2008
- [j39]Thierry Coquand, Henri Lombardi:
A note on the axiomatisation of real numbers. Math. Log. Q. 54(3): 224-228 (2008) - [c39]Thierry Coquand:
Constructive Mathematics and Functional Programming (Abstract). ESOP 2008: 146-147 - [c38]Andreas Abel, Thierry Coquand, Peter Dybjer:
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13 - [c37]Andreas Abel, Thierry Coquand, Peter Dybjer:
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56 - 2007
- [j38]Thierry Coquand:
The Completeness of Typing for Context-Semantics. Fundam. Informaticae 77(4): 293-301 (2007) - [j37]Andreas Abel, Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. Fundam. Informaticae 77(4): 345-395 (2007) - [j36]Thierry Coquand, Arnaud Spiwack:
A proof of strong normalisation using domain theory. Log. Methods Comput. Sci. 3(4) (2007) - [c36]Andreas Abel, Thierry Coquand, Peter Dybjer:
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12 - [c35]Thierry Coquand, Arnaud Spiwack:
Towards Constructive Homological Algebra in Type Theory. Calculemus/MKM 2007: 40-54 - [i4]Thierry Coquand, Arnaud Spiwack:
A proof of strong normalisation using domain theory. CoRR abs/0709.1401 (2007) - 2006
- [j35]Bernhard Banaschewski, Thierry Coquand, Giovanni Sambin:
Preface. Ann. Pure Appl. Log. 137(1-3): 1-2 (2006) - [j34]Gilles Barthe, Thierry Coquand:
Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16(2): 137-155 (2006) - [j33]Thierry Coquand, Henri Lombardi:
A logical approach to abstract algebra. Math. Struct. Comput. Sci. 16(5): 885-900 (2006) - [c34]Thierry Coquand, Arnaud Spiwack:
A Proof of Strong Normalisation using Domain Theory. LICS 2006: 307-316 - [p2]Thierry Coquand:
Alfa/Agda. The Seventeen Provers of the World 2006: 50-54 - [e2]Thierry Coquand, Henri Lombardi, Marie-Françoise Roy:
Mathematics, Algorithms, Proofs, 9.-14. January 2005. Dagstuhl Seminar Proceedings 05021, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006 [contents] - 2005
- [j32]Thierry Coquand, Randy Pollack, Makoto Takeyama:
A Logical Framework with Dependently Typed Records. Fundam. Informaticae 65(1-2): 113-134 (2005) - [j31]Thierry Coquand, Bas Spitters:
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. Univers. Comput. Sci. 11(12): 1932-1944 (2005) - [j30]Thierry Coquand, Bas Spitters:
A constructive proof of the Peter-Weyl theorem. Math. Log. Q. 51(4): 351-359 (2005) - [j29]Thierry Coquand, Henri Lombardi:
A Short Proof for the Krull Dimension of a Polynomial Ring. Am. Math. Mon. 112(9): 826-829 (2005) - [c33]Thierry Coquand:
A Logical Approach to Abstract Algebra. CiE 2005: 86-95 - [c32]Andreas Abel, Thierry Coquand, Ulf Norell:
Connecting a Logical Framework to a First-Order Logic Prover. FroCoS 2005: 285-301 - [c31]Stefano Berardi, Thierry Coquand, Susumu Hayashi:
Games with 1-backtracking. GALOP@ETAPS 2005: 210-225 - [c30]Marc Bezem, Thierry Coquand:
Automating Coherent Logic. LPAR 2005: 246-260 - [c29]Thierry Coquand:
Completeness Theorems and lambda-Calculus. TLCA 2005: 1-9 - [c28]Andreas Abel, Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. TLCA 2005: 23-38 - [p1]Thierry Coquand, Henri Lombardi, Marie-Françoise Roy:
An elementary characterisation of Krull dimension. From sets and types to topology and analysis 2005 - [i3]Thierry Coquand:
05021 Executive Summary -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005 - [i2]Thierry Coquand, Henri Lombardi, Marie-Françoise Roy:
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs. Mathematics, Algorithms, Proofs 2005 - [i1]Thierry Coquand, Henri Lombardi, Peter Schuster:
A Nilregular Element Property. Mathematics, Algorithms, Proofs 2005 - 2004
- [j28]Sara Negri, Jan von Plato, Thierry Coquand:
Proof-theoretical analysis of order relations. Arch. Math. Log. 43(3): 297-310 (2004) - [c27]Ana Bove, Thierry Coquand:
Formalising Bitonic Sort in Type Theory. TYPES 2004: 82-97 - 2003
- [j27]Thierry Coquand, Giovanni Sambin, Jan M. Smith, Silvio Valentini:
Inductively generated formal topologies. Ann. Pure Appl. Log. 124(1-3): 71-106 (2003) - [j26]Marc Bezem, Thierry Coquand:
Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. Bull. EATCS 79: 86-100 (2003) - [j25]Thierry Coquand:
A syntactical proof of the Marriage Lemma. Theor. Comput. Sci. 290(1): 1107-1113 (2003) - [j24]Thierry Coquand, Guo-Qiang Zhang:
A representation of stably compact spaces, and patch topology. Theor. Comput. Sci. 305(1-3): 77-84 (2003) - [c26]Thierry Coquand:
Dynamical Method in Algebra: A Survey. TABLEAUX 2003: 2 - [c25]Thierry Coquand, Randy Pollack, Makoto Takeyama:
A Logical Framework with Dependently Typed Records. TLCA 2003: 105-119 - 2002
- [j23]Thierry Coquand, Erik Palmgren:
Metric Boolean algebras and constructive measure theory. Arch. Math. Log. 41(7): 687-704 (2002) - 2001
- [c24]Thorsten Altenkirch, Thierry Coquand:
A Finitary Subsystem of the Polymorphic lambda-Calculus. TLCA 2001: 22-28 - 2000
- [j22]Thierry Coquand, Erik Palmgren:
Intuitionistic choice and classical logic. Arch. Math. Log. 39(1): 53-74 (2000) - [j21]Thierry Coquand, Sara Sadocco, Giovanni Sambin, Jan M. Smith:
Formal Topologies on The Set of First-Order Formulae. J. Symb. Log. 65(3): 1183-1192 (2000) - [c23]Gilles Barthe, Thierry Coquand:
An Introduction to Dependent Type Theory. APPSEM 2000: 1-41 - [c22]Thierry Coquand, Guo-Qiang Zhang:
Sequents, Frames, and Completeness. CSL 2000: 277-291 - [c21]Thierry Coquand, Makoto Takeyama:
An Implementation of Type: Type. TYPES 2000: 53-62 - [e1]Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith:
Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers. Lecture Notes in Computer Science 1956, Springer 2000, ISBN 3-540-41517-3 [contents]
1990 – 1999
- 1999
- [j20]Thierry Coquand:
A Boolean Model of Ultrafilters. Ann. Pure Appl. Log. 99(1-3): 231-239 (1999) - [j19]Thierry Coquand, Martin Hofmann:
A new method for establishing conservativity of classical systems over their intuitionistic version. Math. Struct. Comput. Sci. 9(4): 323-333 (1999) - 1998
- [j18]Thierry Coquand:
Two applications of Boolean models. Arch. Math. Log. 37(3): 143-147 (1998) - [j17]Stefano Berardi, Marc Bezem, Thierry Coquand:
On the Computational Content of the Axiom of Choice. J. Symb. Log. 63(2): 600-622 (1998) - [c20]Thierry Coquand, Henrik Persson:
Gröbner Bases in Type Theory. TYPES 1998: 33-46 - [c19]Thierry Coquand:
A Note on Formal Iterated Function Systems. RealComp 1998: 2-12 - 1997
- [j16]Thierry Coquand:
Minimal Invariant Spaces in Formal Topology. J. Symb. Log. 62(3): 689-698 (1997) - [j15]Thierry Coquand, Peter Dybjer:
Intuitionistic Model Constructions and Normalization Proofs. Math. Struct. Comput. Sci. 7(1): 75-94 (1997) - [c18]