Defining Algebraic Effects and Handlers via Trails and Metacontinuations

Kenichi Asai and Maika Fujii

October 14, 2025

Code for the paper:

Kenichi Asai and Maika Fujii, ``Defining Algebraic Effects and Handlers via Trails and Metacontinuations,'' Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OlivierFest '25), pp. 26-39 (October 2025). ACM DL

Used environments:

OCaml 4.14.2
Agda 2.7.0.1, standard library 1.7

All the files in a zip file.

Functional derivation

lambda H (left to right)

1def/: definitional interpreter (Figure 5)
2defunc/: defunctionalized interpreter
3linear/: linearized interpreter
4stack/: interpreter with stack
5delinear/: delinearized interpreter
6defunc/: abstract machine (Figure 7)

lambda H' (left to right)

1def/: definitional interpreter (Figure 6)
2defunc/: defunctionalized interpreter
3linear/: linearized interpreter
4stack/: interpreter with stack
5delinear/: delinearized interpreter
6defunc/: abstract machine

lambda H (right to left; not in the paper)

1def/: definitional interpreter
2defunc/: defunctionalized interpreter
3linear/: linearized interpreter
4stack/: interpreter with stack
5delinear/: delinearized interpreter
6defunc/: abstract machine

lambda H' (right to left; not in the paper)

1def/: definitional interpreter
2defunc/: defunctionalized interpreter
3linear/: linearized interpreter
4stack/: interpreter with stack
5delinear/: delinearized interpreter
6defunc/: abstract machine

Agda code for the type systems

lambda H (Figures 8, 9, 10, 11, 12, 13)
lambda H' (Figures 8, 9, 14, 15, 12, 13)

This document was translated from L^AT_EX by H^EV^EA.