POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 10:30 - 10:55 at Auditorium - Type Systems 3 Chair(s): Derek Dreyer

A notion of dimension in intersection typed lambda-calculi is presented. The dimension of a typed lambda-term is given by the minimal norm of an elaboration (a proof theoretic decoration) necessary for typing the term at its type, and, intuitively, measures intersection introduction as a resource.

Bounded-dimensional intersection type calculi are shown to enjoy subject reduction, since terms can be elaborated in non-increasing norm under beta-reduction. We prove that a multiset interpretation (corresponding to a non-idempotent and non-linear interpretation of intersection) of dimensionality corresponds to the number of simulateneous constraints required during search for inhabitants. As a consequence, the inhabitation problem is decidable in bounded multiset dimension, and it is proven to be EXPSPACE-complete. This result is a substantial generalization of inhabitation for the rank 2-fragment, yielding a calculus with decidable inhabitation which is independent of rank.

Our results give rise to a new criterion (dimensional bound) for subclasses of intersection type calculi with a decidable inhabitation problem, which is orthogonal to previously known criteria. Additionally, our notion of dimension should be of interest as a proof theoretic measure of complexity, and we give examples of dimensional analysis of some well-known fragments of the intersection type system, including conservativity over simple types, rank 2-types, and normal form typings.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Type Systems 3POPL at Auditorium
Chair(s): Derek Dreyer MPI-SWS
10:30
25m
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55
25m
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
11:20
25m
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45
25m
Talk
Type Systems as Macros
POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University