Commit d97ee7d
feat(spec): add Phase 1 formal specifications for TypeLL type system
Create the three highest-priority specification documents for TypeLL Phase 1:
1. Verification Protocol (spec/protocol/TYPELL-PROTOCOL.adoc) — defines the
REST/JSON API schema including all 12 endpoints, request/response types,
CheckContext routing, CheckResult schema, error codes, and security
considerations. Documents the wire format consumed by PanLL's TypeLLCmd.res.
2. Dependent Types (spec/type-system/dependent.adoc) — formal typing rules
for Pi types, Sigma types, type-level term arithmetic, refinement types
with predicate decision procedures, universe polymorphism, proof obligation
generation, and dimensional types. Maps all rules to Rust implementation.
3. Linear Types (spec/type-system/linear.adoc) — formal QTT substructural
rules including the {0, 1, omega, n} semiring, context splitting/scaling,
usage tracking lifecycle, linear vs affine mode semantics, and interaction
with dependent types (erased arguments, session type linearity).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>1 parent 0344a34 commit d97ee7d
3 files changed
Lines changed: 2516 additions & 0 deletions
0 commit comments