We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a newly introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.
Tue 1 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:45 - 12:30 | |||
10:45 21mTalk | Mono Types — First-Class Containers for Datalog Technical Papers | ||
11:06 21mTalk | Monadic type-and-effect soundness Technical Papers Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa | ||
11:27 21mTalk | An Effectful Object Calculus Technical Papers Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa | ||
11:48 21mTalk | Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness Technical Papers Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London DOI | ||
12:09 21mTalk | Practical Type-Based Taint Checking and InferenceRemote Technical Papers Nima Karimipour University of California, Riverside, Kanak Das University of California, Riverside, Manu Sridharan University of California at Riverside, Behnaz Hassanshahi Oracle Labs, Australia | ||