Algebraic Effects and Handlers for Arrows in Lean

A Lean 4 formalization of Algebraic Effects and Handlers for Arrows.

The development includes:

• intrinsically typed terms, commands, and handlers;
• externally supplied base types and operation signatures;
• renaming and simultaneous substitution for the two typing contexts;
• call-by-value operational semantics, progress, and normal-form results;
• profunctors, strong promonads, and a universe-small free-arrow model;
• abstract and parameterized denotational semantics;
• one-step and multi-step soundness;
• a logical-relations fundamental theorem and closed-unit adequacy.

Project structure

• ArrowEffectHandler/Core.lean: types, contexts, variables, and signatures
• ArrowEffectHandler/Syntax.lean: terms, commands, and handlers
• ArrowEffectHandler/OperationalSemantics/: reduction and continuations
• ArrowEffectHandler/CategoryTheory/: categorical infrastructure and the free-arrow model
• ArrowEffectHandler/DenotationalSemantics/: interpretations, soundness, and adequacy
• ArrowEffectHandler/Examples/: concrete examples

Import the complete public API with:

import ArrowEffectHandler

Building

The project is pinned to Lean 4.28.0 and Mathlib 4.28.0.

lake build

License

MIT