Cross-reference glossary for README.adoc, EXPLAINME.adoc, and the Typell wiki.
- Verification kernel
-
Typell’s core: the type checker, proof engine, effect tracker, and session manager. Implemented in Rust, specified in Idris 2. See also: [spec-implementation-alignment]
- Spec-implementation alignment
-
The obligation that the Rust kernel faithfully implements the Idris 2 formal specification. Not machine-checked; maintained manually via FFI bridge and generated headers.
- JSON-RPC verification protocol
-
The language-agnostic interface through which consumers (PanLL, VS Code, CLI) interact with Typell.
- Quantitative Type Theory (QTT)
-
Idris 2’s core theory: dependent types with resource quantities tracked in the type. Generalises linear types (0 or 1 uses) to arbitrary semiring-graded usage.
- Proof-carrying code
-
Architecture where compiled code carries cryptographic proof certificates that can be verified independently of the compiler. (Necula, 1998).
- Session protocol manager
-
Typell component enforcing session types: connections close, transactions are atomic, handshake order is followed.
- VCL-dt++
-
Typell backend for VeriSimDB. Port from ReScript. Target: 8-modality queries, cross-modal proofs, hexad types.
- GPNL-dt++
-
Typell backend for LithoGlyph. Bridge to Lean 4. Target: knowledge graphs, RATIONALE clause, refinement types.
- KRL-dt++
-
Typell backend for QuandleDB. Design from scratch. Target: category-theoretic schema, equality saturation, HoTT equality.
- Idris 2 specs (
src/abi/) -
The formal specification layer. Types and soundness proofs written in Idris 2, consuming no
believe_me.
- Rust kernel (
src/kernel/) -
The implementation layer. Chosen for performance, memory safety, and Tauri compatibility with PanLL.
- Zig FFI (
ffi/zig/) -
The C ABI compatibility layer. Bridges the Idris 2 specs and Rust kernel to external consumers via the hyperpolymath universal standard.