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 (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Type Systems 3 at Auditorium
Chair(s): Derek DreyerMPI-SWS
POPL-2017-papers10:30 - 10:55
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
POPL-2017-papers10:55 - 11:20
Nada AminEPFL, Tiark RompfPurdue University
POPL-2017-papers11:20 - 11:45
Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
POPL-2017-papers11:45 - 12:10
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University