milner b519a277c3 add(substitution): substitution distributes over applications and explicit substitutions (M2 support)

2026-09-22 14:17:00 +02:00

..

Binding.v

add(binding): locally nameless opening closing lifting and substitution laws (M1 obligations)

2026-09-22 09:50:00 +02:00

dune

initial commit: confluence and normalisation

2026-09-22 09:20:00 +02:00

ExecReducer.v

initial commit: confluence and normalisation

2026-09-22 09:20:00 +02:00

Metatheory.v

add(metatheory): nonempty reduction closure free variable preservation full composition and beta simulation (M2)

2026-09-22 11:40:00 +02:00

Reduction.v

add(reduction): full completeness and a decision procedure for one step reduction (context composition over positions)

2026-09-22 11:02:00 +02:00

Substitution.v

add(substitution): substitution distributes over applications and explicit substitutions (M2 support)

2026-09-22 14:17:00 +02:00

Subsystem.v

add(subsystem): occurrence count per explicit substitution and the absence of a critical overlap between R and Gc (M3 infrastructure)

2026-09-22 13:49:00 +02:00

Tests.v

add(tests): bounded conformance suite for the reducer against the relational semantics (golden corpus)

2026-09-22 12:17:00 +02:00