Operational game semantics for generative algebraic effects and handlers
This paper provides a fully abstract trace semantics for a typed call-by-value λ-calculus with algebraic effects and handlers. This language is equipped with dynamic allocation of effect instances, which are first-class values and can be exchanged. Our trace model is built using an operational presentation of game semantics, where traces represents the interaction between the program and any environment.
Mon 4 SepDisplayed time zone: Pacific Time (US & Canada) change
09:00 - 10:30
|One Weird Trick to Untie Landin's Knot|
|Operational game semantics for generative algebraic effects and handlersRemote|
|Higher-Order Weakest Precondition Transformers via a CPS Transformation|
Satoshi Kura National Institute of InformaticsPre-print