Wed 10 Jan 2018 11:20 - 11:45 at Watercourt - Types and Effects Chair(s): Neel Krishnaswami

We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar’s effect theories, whose dependently typed operations allow us to capture precise notions of computation, e.g., state with location-dependent store types and dependently typed update monads. Our treatment of handlers is based on an observation that their conventional term-level definition leads to unsound program equivalences being derivable in languages that include a notion of homomorphism. We solve this problem by giving handlers a novel type-based treatment via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations), capturing Plotkin and Pretnar’s insight that handlers denote algebras. We show that the conventional presentation of handlers can then be routinely derived. We also demonstrate that this type-based treatment of handlers provides a useful mechanism for reasoning about effectful computations.

Wed 10 Jan

POPL-2018-papers
10:30 - 12:10: Research Papers - Types and Effects at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
POPL-2018-papers10:30 - 10:55
Talk
Jean-Philippe BernardyUniversity of Gothenburg, Mathieu BoespflugTweag I/O, Ryan R. NewtonIndiana University, Simon Peyton JonesMicrosoft Research, Arnaud SpiwackTweag I/O
Pre-print File Attached
POPL-2018-papers10:55 - 11:20
Talk
POPL-2018-papers11:20 - 11:45
Talk
Danel AhmanInria Paris
POPL-2018-papers11:45 - 12:10
Talk
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław