Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 16:27 - 16:49 at Sala I - Type Inference II Chair(s): Niki Vazou

We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides an algebraic and algorithmic theory of approximation of classical principal types in terms of computable bases of abstract vector spaces (more precisely, semimodules), and it shows a systematic connection of dimensional calculi to the theory of approximants. Finite, computable bases are shown to span standard principal typings of a given term for sufficiently high dimension, thereby providing an approximation to standard principality by type inference, and capturing it precisely for sufficiently large dimensional parameter. Subsidiary results include decidability of principal inhabitation for intersection types (given a type does there exist a normal form for which the type is principal?). Remarkably, combining bounded type inference with principal inhabitation allows us to compute approximate normal forms of arbitrary terms without using beta-reduction.

Presentation Slides (slidesPOPL19_Dudenhefner.pdf)139KiB

Thu 17 Jan

Displayed time zone: Belfast change

15:21 - 16:49
Type Inference IIResearch Papers at Sala I
Chair(s): Niki Vazou IMDEA Software Institute
15:21
22m
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke Miyazaki Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Gradual Typing: A New Perspective
Research Papers
Giuseppe Castagna CNRS - Université Paris Diderot, France, Victor Lanvin IRIF, Université Paris Diderot, France, Tommaso Petrucciani DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. Siek Indiana University, USA
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal Lago University of Bologna, Italy / Inria, France, Marc De Visme ENS Lyon, Damiano Mazza CNRS, Akira Yoshimizu INRIA
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
Principality and Approximation under Dimensional Bound
Research Papers
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
Link to publication DOI Media Attached File Attached