This is a formalisation of the core λeff calculus from the Handlers in action
preprint by Kammar, Lindley and Oury. At present it only contains the
operational semantics. The definition is written in
Ott and the Makefile produces Coq and
Isabelle/HOL definitions. There are some example terms in the HandlersEx.*
files, and some code to execute them in HandlersResults.*.
The libraries and preprint for the actual paper can be found at [https://github.com/slindley/effect-handlers].