Revisiting the categorical interpretation of dependent type theory

Pierre Louis Curien; Richard Garner; Martin Hofmann

doi:10.1016/j.tcs.2014.03.003

Revisiting the categorical interpretation of dependent type theory

Pierre Louis Curien^*, Richard Garner, Martin Hofmann

^*Corresponding author for this work

Research output: Contribution to journal › Article

4 Citations (Scopus)

Abstract

We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

Original language	English
Pages (from-to)	99-119
Number of pages	21
Journal	Theoretical Computer Science
Volume	546
DOIs	https://doi.org/10.1016/j.tcs.2014.03.003
Publication status	Published - 21 Aug 2014

Access to Document

10.1016/j.tcs.2014.03.003

Link to publication in Scopus

Fingerprint Dive into the research topics of 'Revisiting the categorical interpretation of dependent type theory'. Together they form a unique fingerprint.

Cite this

@article{bc8e192f886f40ca8fc039a04a8d1c2b,

title = "Revisiting the categorical interpretation of dependent type theory",

abstract = "We show that Hofmann's and Curien's interpretations of Martin-L{\"o}f's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.",

author = "Curien, {Pierre Louis} and Richard Garner and Martin Hofmann",

year = "2014",

month = "8",

day = "21",

doi = "10.1016/j.tcs.2014.03.003",

language = "English",

volume = "546",

pages = "99--119",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Revisiting the categorical interpretation of dependent type theory

AU - Curien, Pierre Louis

AU - Garner, Richard

AU - Hofmann, Martin

PY - 2014/8/21

Y1 - 2014/8/21

N2 - We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

AB - We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

UR - http://www.scopus.com/inward/record.url?scp=84926689015&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2014.03.003

DO - 10.1016/j.tcs.2014.03.003

M3 - Article

VL - 546

SP - 99

EP - 119

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -