A Fine Calculus for Static Delimited Control

This repository develops a call-by-value λ-calculus with static delimited control, shared prompts, and reductions that exploit statically known continuations. Delimiters carry data, which supports dynamic binding and deep effect handlers.

The paper source is in tex/fc.tex; the mechanizations use Abella and Rocq.

Rocq development

The active Rocq proof is split by responsibility:

• coq-shared-prompts/SharedPrompts.v defines syntax, lifting, substitution, contexts, and the reference reduction.
• coq-let-s-normalization/StructuralReduction.v defines the contextual closures of let-shift and right-associating let.
• coq-let-s-normalization/DeGrooteNormalization.v proves strong normalization of let-shift alone.
• coq-let-s-normalization/WeightedMeasures.v, WeightedNormalization.v, and LetAssociationNormalization.v prove joint normalization of let-shift and let association.
• AdministrativeReduction.v defines the two-mode presentation: admin_step is closed under all term constructors, while tail_step κ descends only through let bodies below continuation κ.
• AdministrativeAlgebra.v contains lifting, renaming, and replacement algebra.
• AdministrativeResiduals.v contains derived valleys and mixed-peak gadgets.
• FrameCompatibility.v proves compatibility with installed one-let frames.
• AdministrativeMeasures.v establishes the measure profiles used for termination. Its per-rule contextual relations are proof devices, not an alternative operational semantics.
• AdministrativeNormalization.v proves termination directly for admin_step.
• AdministrativeConfluence.v proves local confluence by mutual induction over one-step peaks and derives confluence by Newman's lemma.
• coq-shared-prompts/CoreParallel.v defines parallel reduction for the lambda/control core with a scoped payload environment; CoreParallelCompatibility.v proves its diamond property.

The headline results are:

• admin_step_locally_confluent;
• admin_step_confluent (by Newman's lemma);
• admin_strongly_normalizing;
• admin_values_strongly_normalizing.

The administrative results are closed under Rocq's global context: they use no axioms or section hypotheses. core_parallel_diamond currently uses functional extensionality through its substitution algebra.

Build everything with:

opam exec -- dune build -j 1

Abella development

The original Abella development is in abella/. It targets Abella commit c17cb187.