Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Typability in bounded dimension
 Aceto, L. ; Association for Computing Machinery ACM; Institute of Electrical and Electronics Engineers IEEE: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 : 2023 June 2017, Reykjavík, Iceland Piscataway, NJ: IEEE, 2017 ISBN: 9781509030187 ISBN: 9781509030194 Art. 67, 12 pp. 
 Symposium on Logic in Computer Science (LICS) <32, 2017, Reykjavík> 

 English 
 Conference Paper 
 Fraunhofer ISST () 
Abstract
Recently (authors, POPL 2017), a notion of dimensionality for intersection types was introduced, and it was shown that the boundeddimensional inhabitation problem is decidable under a nonidempotent interpretation of intersection and undecidable in the standard settheoretic model. In this paper we study the typability problem for boundeddimensional intersection types and prove that the problem is decidable in both models. We establish a number of bounding principles depending on dimension. In particular, it is shown that dimensional bound on derivations gives rise to a bounded width property on types, which is related to a generalized subformula property for typings of arbitrary terms. Using the bounded width property we can construct a nondeterministic transformation of the typability problem to unification, and we prove that typability in the settheoretic model is PSPACEcomplete, whereas it is in NP in the multiset model.