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:4521m Talk | Mono Types — First-Class Containers for Datalog Technical Papers | ||
| 11:0621m Talk | Monadic type-and-effect soundness Technical Papers Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa | ||
| 11:2721m Talk | An Effectful Object Calculus Technical Papers Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa | ||
| 11:4821m Talk | 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 LondonDOI | ||
| 12:0921m Talk | 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 | ||

