Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Publikationen / On the Interpretation of Type Theory in Locally Cartesian Closed Categories


Inhaltsbereich

Martin Hofmann (1994)

On the Interpretation of Type Theory in Locally Cartesian Closed Categories

In: Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, ed. by Leszek Pacholski and Jerzy Tiuryn, vol. 933, pp. 427-441, Springer. Lecture Notes in Computer Science (ISBN: 3-540-60017-5).

We show how to construct a model of dependent type theory (category with attributes) from a locally cartesian closed category (lccc). This allows to define a semantic function interpreting the syntax of type theory in an lccc. We sketch an application which gives rise to an interpretation of extensional type theory in intensional type theory.

Artikelaktionen


Funktionsleiste