COPLAS talk by Jakob Rehof: Dimensional Intersection Type Calculi

On 30 August 2018, Prof. Dr. Jakob Rehof, Technical University of Dortmund and Fraunhofer Institute for Software and Systems Engineering, will give a talk on Dimensional Intersection Type Calculi.


Recently (POPL 2017, LICS 2017) we introduced a concept of dimensionality for intersection types, which can be seen as a parametric bounding principle that is orthogonal to principles based on type-theoretic rank. Briefly, 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.

In this talk we will give an overview of the theory of dimension for intersection type calculi and main results concerning decidability and complexity of the classical type-theoretic decision problems (inhabitation and typability) under dimensional bound. 



All are welcome. No registration required.  

Note: There is another COPLAS talk, by Mark Giesbrecht on symbolic computation, immediately after this one.