Contents
Every page of the site, by section.
Semantics evidencesemantics
- Semantics evidence
- Open work
- Store Typing
- Residual Program Typing
- Scope Lifetime & Finalization
- Reactive Scheduling
- Exact Codecs
- Subtyping Algebra
- Initial Algebras & Folds
- Context Requirements
- Host Session Protocol
- Translation & Simulation
- Applicability decisions
- Placement
- Plan
- R1: The signature is a parameter: one located refusal admits Σ_app, and every milestone statement takes it · in Plan
- R2: Extension is conservative: C1–C8 over DI-47's relation on Σ_app · in Plan
- R3: Data: the type language closed under records and variants as Ty growth · in Plan
- R4: State: the world types every cell at any type, with rows as templates · in Plan
- R5: Services: the service table, layers and provision · in Plan
- R6: The host: a lawful HostSpec, receipt and application, DI-57's table-aware reference · in Plan
- R7: Retained behaviour: a resolved code entry is typed at its reference's type · in Plan
- R8: Runs and faces as named connections: equal to the reference inside a profile, refused outside it · in Plan
- R9: Never goes wrong: M7a–c on M7Fragment (the empty host table, answer-free tapes) · in Plan
- R10: Library code inherits theorems: a composed module's law is Agrees profile module expansion · in Plan
- R11: Resources are released: at most once per registration, exactly once in close order · in Plan
- R12: Frontiers name what they await · in Plan
- R13: A run's inputs are data: equal recorded inputs give equal replay observations · in Plan
- R14: A sketch checks and explains its types: holes and the gap, graduality, the focus, minimal type slices and total marking · in Plan
- Acceptance programs