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

• 1) give an introduction to the problem of combining linearity and type dependency
• 2) present a solution to the problem, primarily from the point of view of categorical semantics
• 3) sketch how this analysis has led to a coherence space and game semantics of dependent type theory.