Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Intersection type calculi of bounded dimension
 Castagna, G. ; Association for Computing Machinery ACM; Association for Computing Machinery ACM, Special Interest Group on Programming Languages SIGPLAN; Association for Computing Machinery ACM, Special Interest Group on Algorithms and Computation Theory SIGACT: POPL 2017, 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Proceedings : Paris, France, January 1521, 2017 New York: ACM, 2017 ISBN: 9781450346603 pp.653665 
 Symposium on Principles of Programming Languages (POPL) <44, 2017, Paris> 

 English 
 Conference Paper 
 Fraunhofer ISST () 
Abstract
A notion of dimension in intersection typed λcalculi is presented. The dimension of a typed λ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. Boundeddimensional intersection type calculi are shown to enjoy subject reduction, since terms can be elaborated in nonincreasing norm under βreduction. We prove that a multiset interpretation (corresponding to a nonidempotent and nonlinear interpretation of intersection) of dimensionality corresponds to the number of simultaneous constraints required during search for inhabitants. As a consequence, the inhabitation problem is decidable in bounded multiset dimension, and it is proven to be EXPSPACEcomplete. This result is a substantial generalization of inhabitation for the rank 2fragment, 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, and which should have immediate applications in synthesis. Additionally, we give examples of dimensional analysis of fragments of the intersection type system, including conservativity over simple types, rank 2types, and normal form typings, and we provide some observations towards dimensional analysis of other systems. It is suggested (for future work) that our notion of dimension may have semantic interpretations in terms of of reduction complexity.