CS SEMINAR

Dimensional Intersection Type Calculi

Speaker
Professor Jakob Rehof, University of Dortmund
Chaired by
Dr Abhik ROYCHOUDHURY, Provost's Chair Professor, School of Computing
abhik@comp.nus.edu.sg

29 Aug 2019 Thursday, 02:00 PM to 03:00 PM

Executive Classroom, COM2-04-02

Abstract:

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.


Biodata:

Since 2006 Jakob Rehof holds a joint position as full professor of Computer Science at the University of Dortmund, where he is chair of Software Engineering, and as director of the Fraunhofer Institute for Software and Systems Engineering (ISST) Dortmund. Jakob Rehof studied Computer Science and Mathematics at the University of Copenhagen and got his Ph.D. in Computer Science at DIKU, Department of Computer Science, University of Copenhagen. In 1997 Rehof was a visiting Researcher at the University of Stanford, CA, USA. From 1998 until 2006 he was at Microsoft Research, Redmond, WA, USA.

Prior to all of the above he studied Classical Philology (Latin & Greek) and Philosophy at the University of Aarhus and the University of Copenhagen and was a DAAD scholar at the Eberhard-Karls University of Tubingen.