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

We introduce a type system for the $\pi$-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e. to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is $\Pi^0_2$-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

 Slides of the talk "Intersection Types and Runtime Errors in the Pi-Calculus" (IT.pdf) 159KiB

#### 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:43Talk Dynamic Type Inference for Gradual Hindley–Milner TypingResearch PapersYusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan Link to publication DOI Pre-print Media Attached File Attached 15:43 - 16:05Talk Gradual Typing: A New PerspectiveResearch PapersGiuseppe 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:27Talk Intersection Types and Runtime Errors in the Pi-CalculusResearch PapersUgo 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:49Talk Principality and Approximation under Dimensional BoundResearch PapersAndrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund Link to publication DOI Media Attached File Attached