Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Fri 4 Nov 2016 11:20 - 11:45 at Matterhorn 1 - Typing, in Practice Chair(s): Sebastian Erdweg

This paper introduces a novel type-and-effect calculus, first-class effects, where the computational effect of an expression can be programmatically reflected, passed around as values, and analyzed at run time. A broad range of designs "hard-coded" in existing effect-guided analyses — from thread scheduling, version-consistent software updating, to data zeroing — can be naturally supported through the programming abstractions. The core technical development is a type system with a number of features, including a hybrid type system that integrates static and dynamic effect analyses, a refinement type system to verify application-specific effect management properties, a double-bounded type system that computes both over-approximation of effects and their under-approximation. We introduce and establish a notion of soundness called trace consistency, defined in terms of how the effect and trace correspond. The property sheds foundational insight on "good" first-class effect programming.

Fri 4 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Typing, in PracticeOOPSLA at Matterhorn 1
Chair(s): Sebastian Erdweg Delft University of Technology, Netherlands
10:30
25m
Talk
A Practical Framework for Type Inference Error Explanation
OOPSLA
Calvin Loncaric University of Washington, Satish Chandra Samsung Research America, Manu Sridharan Samsung Research America, Cole Schlesinger Samsung Research America
DOI Pre-print Media Attached
10:55
25m
Talk
Dynamically Diagnosing Type Errors in Unsafe CodeAEC
OOPSLA
Stephen Kell University of Cambridge
DOI Media Attached
11:20
25m
Talk
First-Class Effect Reflection for Effect-Guided Programming
OOPSLA
Yuheng Long Iowa State University, Yu David Liu , Hridesh Rajan Iowa State University, USA
DOI
11:45
25m
Talk
Java and Scala's Type Systems are Unsound: The Existential Crisis of Null PointersAEC
OOPSLA
Nada Amin EPFL, Ross Tate Cornell University
Link to publication DOI Pre-print