Specification and Verification for Unrestricted Algebraic Effects and Handling
![Thumbnail](http://memento.epfl.ch/image/28351/1440x810.jpg)
Event details
Date | 10.09.2024 |
Hour | 11:00 › 12:00 |
Location | |
Category | Conferences - Seminars |
Event Language | English |
by Dr Yahui Song, Research Fellow from National University of Singapore (NUS)
Abstract
Abstract
Programming with user-defined effects and effect handlers has many practical use cases involving imperative effects. Additionally, it is natural and powerful to use multi-shot effect handlers for non-deterministic or probabilistic programs that allow backtracking to compute a comprehensive outcome. Existing works for verifying effect handlers are restricted in one of two ways: permitting multi-shot continuations under pure setting or allowing heap manipulation for only one-shot continuations, due to the employed protocol mechanism to model interactions between invoked effects and their handlers. This work proposes a novel calculus called Effectful Specification Logic (ESL) to support unrestricted effect handlers, where zero-/one-/multi-shot continuations can co-exist with imperative effects and higher-order constructs. ESL captures behaviors in stages, and provides precise models to support invoked effects, handlers and continuations. To show its feasibility, we prototype an automated verification system for this novel specification logic, prove its soundness, report on useful case studies, and present experimental results. With this proposal, we have provided an extended specification logic that is capable of modeling arbitrary imperative higher-order programs with algebraic effects and continuation-enabled handlers.
Bio
Bio
Yahui is a Research Fellow in the Automated Program Repair group at NUS, working with Prof Abhik Roychoudhury and Prof Wei-Ngan Chin. Her research focuses on programming languages, particularly functional programming, specification, and verification, logics such as temporal logic and separation logic, and their applications in bug finding and automated program repair.
More information
More information
Practical information
- General public
- Free
Contact
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch