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 › peer-review

23 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

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 = aug,

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 - https://www.scopus.com/pages/publications/84926689015

U2 - 10.1016/j.tcs.2014.03.003

DO - 10.1016/j.tcs.2014.03.003

M3 - Article

AN - SCOPUS:84926689015

SN - 0304-3975

VL - 546

SP - 99

EP - 119

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

Revisiting the categorical interpretation of dependent type theory

Abstract

Access to Document

Other files and links

Fingerprint

Cite this