ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Thu 9 Jul 2015 13:30 - 14:00 at Bohemia - Type Systems Chair(s): Peter Müller

Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve efficiency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, memoization, security and UI access.

Thu 9 Jul
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00: Type SystemsResearch Track at Bohemia
Chair(s): Peter MüllerETH Zurich
13:30 - 14:00
Intensional Effect Polymorphism
Research Track
Yuheng LongIowa State University, Yu David LiuState University of New York (SUNY) Binghamton, Hridesh RajanIowa State University
14:00 - 14:30
Type Inference for Place-Oblivious Objects
Research Track
Riyaz HaqueUniversity of California, Los Angeles (UCLA), Jens PalsbergUniversity of California, Los Angeles
14:30 - 15:00
Asynchronous Liquid Separation Types
Research Track
Johannes KloosMPI-SWS, Rupak MajumdarMPI-SWS, Viktor VafeiadisMPI-SWS, Germany