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
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

15:21 - 16:49: Research Papers - Type Inference II at Sala I
Chair(s): Niki VazouIMDEA Software Institute
POPL-2019-Research-Papers15:21 - 15:43
Yusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
POPL-2019-Research-Papers15:43 - 16:05
Giuseppe CastagnaCNRS - Université Paris Diderot, France, Victor LanvinIRIF, Université Paris Diderot, France, Tommaso PetruccianiDIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. SiekIndiana University, USA
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers16:05 - 16:27
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers16:27 - 16:49
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
Link to publication DOI Media Attached File Attached