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].