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: Greenwich Mean Time : Belfast change

15:21 - 16:49: Type Inference IIResearch Papers at Sala I
Chair(s): Niki VazouIMDEA Software Institute
15:21 - 15:43
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43 - 16:05
Talk
Gradual Typing: A New Perspective
Research Papers
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
16:05 - 16:27
Talk
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA
Link to publication DOI Media Attached File Attached
16:27 - 16:49
Talk
Principality and Approximation under Dimensional Bound
Research Papers
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
Link to publication DOI Media Attached File Attached