Dynamic intermediates WIP; continuing in literate-execution - #37

Open

rolyp wants to merge 1109 commits into

bobatkey:mainfrom

fluid-org:dynamic-intermediates

This pull request is big! We're only showing the most recent 250 commits

Commits on Jul 11, 2026

Commits on Jul 12, 2026

Onto 2.5.
rolyp
committed

Commits on Jul 17, 2026

Commits on Jul 18, 2026

Add value-level signature algebras.

rolyp
and
claude
committed
Add example signature with value-level interpretation.

rolyp
and
claude
committed
Type-level substitution fusion laws and nested-mu unfolding lemma.

rolyp
and
claude
committed
Big-step operational semantics over mu-types.

rolyp
and
claude
committed
Replace duplicate example signature with value-level algebra for example.signature.

rolyp
and
claude
committed
Matrix-decorated big-step evaluation.

rolyp
and
claude
committed
Trace and dependence-graph tooling over matrix-decorated derivations.

rolyp
and
claude
committed
Skeleton and design for the logical relation module.

rolyp
and
claude
committed
Trim module commentary.

rolyp
and
claude
committed
Strip comments derivable from the code.

rolyp
and
claude
committed
Logical relation and fundamental property statement.

rolyp
and
claude
committed
Action of Mat(S) on free semimodules.

rolyp
and
claude
committed
Instantiate the logical relation: Boolean dependency model over rationals.

rolyp
and
claude
committed
Totality predicate: existence content of the logical relation.

rolyp
and
claude
committed
Acc-irrelevance for the totality predicate.

rolyp
and
claude
committed
Arrow-leaf size bound, preserved by renaming, substitution and unfolding.

rolyp
and
claude
committed
Restore mrel-mu: explicit fibre-subst endpoints fix the stuck unification.

rolyp
and
claude
committed
Conversion between totality at substituted types and the mu family.

rolyp
and
claude
committed
Fundamental lemma for totality; evaluator for closed terms.

rolyp
and
claude
committed
Trace harness at the Boolean model with golden tests.

rolyp
and
claude
committed
Port dump-graphs IO main; ignore GHC build directory.

rolyp
and
claude
committed

Commits on Jul 19, 2026

Commits on Jul 20, 2026

Commits on Jul 21, 2026

Commits on Jul 29, 2026

Commits on Jul 30, 2026