Mon 15 Jul 2019 11:45 - 12:15 at Epernay - Session One

Effect systems are used to statically reason about the effects an expression may have when evaluated. In the literature, such effects include various behaviours as diverse as memory accesses and exception throwing. Here we present CallƐ, an object oriented language that takes a flexible approach where effects are just method calls: this allows ordinary methods to model things such as I/O operations and access to global state. CallƐ supports both flexible and fine-grained control over such behaviour, in a way designed to minimise the complexity of effect annotations.

CallƐ allows OO code to be prevented from performing privileged operations such as exiting the program or performing network communication. It can also be used to ensure determinism, by preventing methods from (indirectly) calling non-deterministic primitives like random number generation or file reading.

Mon 15 Jul
Times are displayed in time zone: Greenwich Mean Time : Belfast change

10:45 - 12:15: Session OneFTfJP at Epernay
10:45 - 11:45
Invited Talk - JayHorn: A Java Model Checker
Philipp RuemmerUppsala University
11:45 - 12:15
CallƐ: An Effect System for Method Calls
Isaac Oscar Gariano, James NobleVictoria University of Wellington, Marco ServettoVictoria University Wellington, New Zealand