English version

PPS UMR 7126 – Laboratoire
Preuves, Programmes et Systèmes

Accueil · Présentation · Membres · Publications · Séminaire · Groupes de travail · Projets · πr²

Splitting the atom of dependent types

Matthijs Vákár (Oxford University)

4 juin 2015 à 10H30

Abstract: Linear logic and game semantics, respectively, provide detailed resource sensitive and operational analyses of intuitionistic logic. Such analyses have been carried out to give deeper insights into a broad range of logics and type theories, e.g. intuitionistic proposional and predicate logic, system F, PCF and languages with various features like recursive types, state and non-local control. One system that had so far defied such a linear and game theoretic analysis is dependent type theory (or Martin-Löf type theory), as there seems to exist a fundamental tension between linearity and type dependency.

In this talk, I will