BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Coquand:Thierry

Contributed to:

TLCA 20152015
TLCA 20132013
CSL 20092009
TLCA 20092009
ESOP 20082008
FLOPS 20082008
LICS 20072007
LICS 20062006
TLCA 20052005
TLCA 20032003
TLCA 20012001
CSL 20002000
CSL 19971997
TLCA 19951995
LICS 19891989
LICS 19881988
LICS 19861986
TAPSOFT, Vol.2: CFLP 19871987
CSL 20162016

Wrote 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.
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.
The Ackermann Award 2016 (TC, AD), p. 4.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.