Coq formalization of the type safety theorem for the calculus from "An Introduction to Algebraic Effects and Handlers" by Matija Pretnar (theorem 4.2 in the paper).
coq_makefile -f _CoqProject *.v -o Makefile
make
*Maps.v file comes from "Software Foundations" book.