Blogs (1) >>
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

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 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 File Attached
POPL-2019-Research-Papers16:27 - 16:49
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
Link to publication DOI File Attached