Revisiting the categorical interpretation of dependent type theory

Pierre Louis Curien*, Richard Garner, Martin Hofmann

*Corresponding author for this work

    Research output: Contribution to journalArticle

    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 languageEnglish
    Pages (from-to)99-119
    Number of pages21
    JournalTheoretical Computer Science
    Volume546
    DOIs
    Publication statusPublished - 21 Aug 2014

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

    Cite this