Links und Funktionen
Sprachumschaltung
Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2011 / Oberseminar / Gabriel Scherer: Universe subtyping in Martin-Löf Type Theory
Inhaltsbereich

Gabriel Scherer: Universe subtyping in Martin-Löf Type Theory

TCS Oberseminar, 22.07.2011, 11:15
Wann 11:15 12:15 22.07.2011
von bis
Wo L109
Termin übernehmen vCal
iCal

Universe subtyping in Martin-Löf Type Theory

In this talk, I will present the current state of our work -- with Andreas Abel -- on the metatheory of dependent type systems with a universe hierarchy.

Our not-yet-reached goal is universe polymorphism, as a potential extension of the Agda system. This means that we have to develop both:

  1. a suitable formalization of universe subtyping and its metatheory
  2. a practical type checking algorithm, along with proofs that the algorithms are faithful to the declarative type system
In the talk I shall focus on the second aspect: how to prove equivalence between a declarative type system and a type checking algorithm. I will try to explain logical relations, the main proof technique that we use -- both to get the usual meta-theoretic results and algorithmic completeness -- in a way that require no previous knowledge besides familiarity with type system definitions.  

 

Artikelaktionen

abgelegt unter:
Funktionsleiste