Glossary and Notation Index
This page defines shared terms and symbols used across the docs and paper-aligned pages. Use it as a stable lookup for terminology and notation.
Core Terms
| Term | Meaning | Primary Docs |
|---|---|---|
| coherence | Session-wide compatibility invariant between local type state, buffers, and global structure. | Theory, Theorem Program |
| harmony | Projection and protocol evolution commute under declared premises. | Theory, Theorem Program |
| projection | Mapping from global choreography to per-role local session types. | Choreographic Projection Patterns |
| local type | Per-role protocol view used for runtime typing and progression. | Theory, Session Lifecycle |
| effect handler | Runtime boundary that interprets VM or choreography actions. | Choreography Effect Handlers, Effect Handlers and Session Types |
| theorem-pack | Lean-exported capability inventory used by runtime admission gates. | Lean Verification, Capability and Admission |
| admission | Runtime gate process that checks contracts and capability evidence. | Capability and Admission |
| envelope | Declared refinement boundary for higher-concurrency and profile-scoped behavior. | VM Architecture, Rust-Lean Parity |
| determinism profile | Runtime trace-equivalence contract mode such as Full or Replay. | VM Architecture, Rust-Lean Parity |
| communication replay mode | Transport replay-consumption policy: off, sequence, or nullifier. | VM Architecture, Session Lifecycle |
| communication nullifier | Domain-separated digest of canonical communication identity used for one-time receive consumption checks. | VM Architecture, Session Lifecycle |
| consumption root | Deterministic accumulator root over communication replay-consumption state. | VM Architecture, Rust-Lean Parity |
Symbol and Notation Index
| Symbol or Form | Meaning | Primary Docs |
|---|---|---|
G | Global protocol type. | Theory |
L or LocalTypeR | Local role protocol type. | Theory, Bytecode Instructions |
project(G, R) | Projection of global type G for role R. | Theory, Choreographic Projection Patterns |
μX. ... X | Recursive protocol form with bound variable X. | Theory |
⊕{...} | Internal choice at the selecting endpoint. | Theory |
&{...} | External choice at the receiving endpoint. | Theory |
!T.S | Send T, then continue as S. | Theory |
?T.S | Receive T, then continue as S. | Theory |
end | Session termination state. | Theory |
Consume | Recursive receiver-side trace alignment kernel used in coherence proofs. | Theory, Theorem Program |
n = 1 | Canonical single-step concurrency regime for exact parity. | VM Architecture, Rust-Lean Parity |
n > 1 | Higher-concurrency regime admitted under envelope and premise-scoped constraints. | VM Architecture, Rust-Lean Parity |
Full, ModuloEffects, ModuloCommutativity, Replay | Runtime determinism profiles. | VM Architecture, Rust-Lean Parity |
off, sequence, nullifier | Communication replay-consumption modes. | VM Architecture, Session Lifecycle |
telltale.comm.identity.v1 | Domain-separation tag for canonical communication identity schema. | VM Architecture |
Notation Consistency Rules
Use one symbol for one concept in a local section. Reintroduce symbols when crossing between theory and runtime notation. Prefer existing symbols from this index unless precision requires a different one.