Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2019 / Oberseminar / Ulrich Schöpp: Semantical Analysis of Contextual Types


Inhaltsbereich

Ulrich Schöpp: Semantical Analysis of Contextual Types

Oberseminarvortrag von Ulrich Schöpp über Semantical Analysis of Contextual Types (joint work in progress with Brigitte Pientka)
Wann 14:15 16:00 29.05.2019
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

Es spricht Ulrich Schöpp über:
Semantical Analysis of Contextual Types
(joint work in progress with Brigitte Pientka)

Abstract:
Higher-order abstract syntax (HOAS) is an elegant and deceptively simple idea of encoding syntax that models binding and scope of variables by piggy-backing on binding in the meta-language. This requires a weak function space in the meta-language that does not admit recursion or pattern matching. An existing approach, as implemented in Beluga, is to nevertheless support recursion over HOAS syntax trees by characterising them together with the context in which they are meaningful as contextual types and to embed contextual types into a computation language that has a strong function space.

This talk reports on work in progress on giving a semantic account of contextual types and of writing computations about them. We build on previous work by Hofmann on modelling higher-order abstract syntax using presheaf categories. We show that these presheaf models already have all the structure needed to model a contextual types over a simply-typed domain language. We present the structure of the presheaf models in terms of their internal dependent type theory. This formulation makes working with type-dependencies manageable and provides an abstract core calculus for the  interpretation of contextual types and computations about them. To also account for contextual types over dependently-typed lambda-calculi, such as the logical framework LF, we then generalise the approach by using presheaves over a Category with Attributes.

Artikelaktionen


Funktionsleiste