default search action
Thierry 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
- 2024
- [c62]Thierry Coquand
:
A Variation of Reynolds-Hurkens Paradox. Logics and Type Systems in Theory and Practice 2024: 111-117 - [p4]Thierry Coquand:
Some Remarks About Dependent Type Theory. The French School of Programming 2024: 175-202 - [i21]Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, Christian Sattler:
The equivariant model structure on cartesian cubical sets. CoRR abs/2406.18497 (2024) - 2023
- [j74]Thierry Coquand:
Reduction Free Normalisation for a proof irrelevant type of propositions. Log. Methods Comput. Sci. 19(3) (2023) - [i20]Thierry Coquand:
A variation of Reynolds-Hurkens Paradox. CoRR abs/2308.16726 (2023) - 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) - [c61]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
Type Theory with Explicit Universe Polymorphism. TYPES 2022: 13:1-13:16 - [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
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31(4): 424-468 (2021) - [j70]Thierry Coquand
Constructive sheaf models of type theory. Math. Struct. Comput. Sci. 31(9): 979-1002 (2021) - [j69]Marc Bezem, Thierry Coquand
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
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
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
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
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
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
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
Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14(4): 26:1-26:16 (2013) - [c47]Nicolai Kraus
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
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
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
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]Thierry Coquand, Henrik Persson:
A Proof-Theoretical Investigation of Zantema's Problem. CSL 1997: 177-188 - 1996
- [j14]Thierry Coquand:
An Algorithm for Type-Checking Dependent Types. Sci. Comput. Program. 26(1-3): 167-177 (1996) - 1995
- [j13]Thierry Coquand:
A Semantics of Evidence for Classical Arithmetic. J. Symb. Log. 60(1): 325-337 (1995) - [c17]Thierry Coquand:
Program Construction in Intuitionistic Type Theory (Abstract). MPC 1995: 49 - [c16]Stefano Berardi, Marc Bezem, Thierry Coquand:
A realization of the negative interpretation of the Axiom of Choice. TLCA 1995: 47-62 - [c15]Thierry Coquand, Jan M. Smith:
An Application of Constructive Completeness. TYPES 1995: 76-84 - 1994
- [j12]Thierry Coquand, Bengt Nordström, Jan M. Smith, Björn von Sydow:
Type Theorie Programming. Bull. EATCS 52: 203-228 (1994) - [j11]Thierry Coquand:
An Analysis of Ramsey's Theorem. Inf. Comput. 110(2): 297-304 (1994) - [j10]Thierry Coquand, Hugo Herbelin:
A - Translation and Looping Combinators in Pure Type Systems. J. Funct. Program. 4(1): 77-88 (1994) - [c14]Thierry Coquand, Peter Dybjer:
Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS 1994: 60-76 - 1993
- [j9]Thierry Coquand:
Another Proof of the Intuitionistic Ramsey Theorem. Theor. Comput. Sci. 115(1): 63-75 (1993) - [c13]Thierry Coquand:
Infinite Objects in Type Theory. TYPES 1993: 62-78 - 1992
- [j8]Thierry Coquand:
The Paradox of Trees in Type Theory. BIT 32(1): 10-14 (1992) - [j7]Thierry Coquand:
An Intuitionistic Proof of Tychonoff's Theorem. J. Symb. Log. 57(1): 28-32 (1992) - 1991
- [j6]Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov
Inheritance as Implicit Coercion. Inf. Comput. 93(1): 172-221 (1991) - [c12]Thierry Coquand:
Constructive Topology and Combinatorics. Constructivity in Computer Science 1991: 159-164 - [c11]Thierry Coquand:
A Direct Proof of the Intuitionistic Ramsey Theorem. Category Theory and Computer Science 1991: 164-172
1980 – 1989
- 1989
- [j5]Thierry Coquand, Carl A. Gunter, Glynn Winskel:
Domain Theoretic Models of Polymorphism. Inf. Comput. 81(2): 123-167 (1989) - [j4]Thierry Coquand:
Categories of Embeddings. Theor. Comput. Sci. 68(3): 221-237 (1989) - [c10]Val Tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov:
Inheritance and Explicit Coercion (Preliminary Report). LICS 1989: 112-129 - 1988
- [j3]Thierry Coquand, Gérard P. Huet:
The Calculus of Constructions. Inf. Comput. 76(2/3): 95-120 (1988) - [j2]Val Tannen, Thierry Coquand:
Extensional Models for Polymorphism. Theor. Comput. Sci. 59: 85-114 (1988) - [c9]Thierry Coquand, Christine Paulin:
Inductively defined types. Conference on Computer Logic 1988: 50-66 - [c8]Thierry Coquand:
Categories of Embeddings. LICS 1988: 256-263 - 1987
- [c7]Thierry Coquand, Thomas Ehrhard:
An Equational Presentation of Higher Order Logic. Category Theory and Computer Science 1987: 40-56 - [c6]Thierry Coquand, Carl A. Gunter, Glynn Winskel:
DI-Domains as a Model of Polymorphism. MFPS 1987: 344-363 - [c5]Val Tannen, Thierry Coquand:
Extensional Models for Polymorphism. TAPSOFT, Vol.2 1987: 291-307 - 1986
- [c4]Thierry Coquand:
An Analysis of Girard's Paradox. LICS 1986: 227-236 - 1985
- [j1]Thierry Coquand, Gérard P. Huet:
A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. J. Symb. Comput. 1(3): 323-328 (1985) - [c3]Thierry Coquand, Gérard P. Huet:
Constructions: A Higher Order Proof System for Mechanizing Mathematics. European Conference on Computer Algebra (1) 1985: 151-184 - [c2]Thierry Coquand:
Sur l'Analogie entre les Propositions et les Types. Combinators and Functional Programming Languages 1985: 71-84 - [c1]Thierry Coquand, Gérard P. Huet:
Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Logic Colloquium 1985: 123-146
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-07-25 19:27 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: