Travelled to:1 × Brazil
1 × Denmark
1 × Germany
1 × Hungary
1 × Portugal
1 × Spain
1 × The Netherlands
2 × Japan
2 × United Kingdom
3 × Poland
3 × USA
Collaborated with:∅ A.Abel T.Altenkirch V.Tannen M.Bezem P.Dybjer A.Spiwack G.Zhang H.Persson A.Dawar E.Parmann M.Pagano R.Pollack M.Takeyama S.Berardi N.Kraus M.H.Escardó C.A.Gunter A.Scedrov
Talks about:type (8) theori (5) proof (4) polymorph (2) framework (2) construct (2) algorithm (2) calculus (2) theorem (2) complet (2)
Person: Thierry Coquand
DBLP: Coquand:Thierry
Contributed to:
20152013
20092009
2008
2008
20072006200520032001200019971995198919881986
19872016Wrote 20 papers:
- TLCA-2015-BezemCP #set
- Non-Constructivity in Kan Simplicial Sets (MB, TC, EP), pp. 92–106.
- TLCA-2013-KrausECA #theorem
- Generalizations of Hedberg’s Theorem (NK, MHE, TC, TA), pp. 173–188.
- CSL-2009-Coquand #type system
- Forcing and Type Theory (TC), p. 2.
- TLCA-2009-AbelCP #algorithm #composition #proving #type system
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
- ESOP-2008-Coquand #functional #programming
- Constructive Mathematics and Functional Programming (TC), pp. 146–147.
- FLOPS-2008-AbelCD #algebra #on the #proving #type system
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
- LICS-2007-AbelCD #evaluation #normalisation #similarity #type system
- Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (AA, TC, PD), pp. 3–12.
- LICS-2006-CoquandS #normalisation #proving #using
- A Proof of Strong Normalisation using Domain Theory (TC, AS), pp. 307–316.
- TLCA-2005-AbelC #algorithm #framework #logic #similarity
- Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs (AA, TC), pp. 23–38.
- TLCA-2005-Coquand #theorem #λ-calculus
- Completeness Theorems and λ-Calculus (TC), pp. 1–9.
- TLCA-2003-CoquandPT #framework #logic
- A Logical Framework with Dependently Typed Records (TC, RP, MT), pp. 105–119.
- TLCA-2001-AltenkirchC #polymorphism #λ-calculus
- A Finitary Subsystem of the Polymorphic λ-Calculus (TA, TC), pp. 22–28.
- CSL-2000-CoquandZ
- Sequents, Frames, and Completeness (TC, GQZ), pp. 277–291.
- CSL-1997-CoquandP #problem
- A Proof-Theoretical Investigation of Zantema’s Problem (TC, HP), pp. 177–188.
- TLCA-1995-BerardiBC #axiom
- A realization of the negative interpretation of the Axiom of Choice (SB, MB, TC), pp. 47–62.
- LICS-1989-Breazu-TannenCGS #inheritance
- Inheritance and Explicit Coercion (VT, TC, CAG, AS), pp. 112–129.
- LICS-1988-Coquand #category theory
- Categories of Embeddings (TC), pp. 256–263.
- LICS-1986-Coquand #analysis
- An Analysis of Girard’s Paradox (TC), pp. 227–236.
- CFLP-1987-TannenC #modelling #morphism #polymorphism
- Extensional Models for Polymorphism (VT, TC), pp. 291–307.
- CSL-2016-CoquandD
- The Ackermann Award 2016 (TC, AD), p. 4.