Skip to content
#

quantitative-type-theory

Star

Here are 2 public repositories matching this topic...

hyperpolymath / my-lang

Sponsor
Star 2

Research language whose affine/QTT core is proved sound twice — Coq and Idris2, axiom-free and CI-gated — with the verified usage-checker ported into the Rust compiler. Nested Solo ⊂ Duet ⊂ Ensemble dialects, session-typed concurrency, echo types for loss that isn't erasure. Early alpha.

programming-language rust open-source language-design proof-engineering verified-compiler linear-types research-software type-systems affine-types hyperpolymath epistemic-infrastructure epistemic-computing quantitative-type-theory veridical-computing equivalence-aware-computing typed-provenance mechanized-matatheory
  • Updated Oct 16, 2026
  • Rust

sjqtentacles / blight

Sponsor
Star 1

A dependently-typed, self-hosting language with a tiny trusted kernel (cubical + quantitative types + effects). Scheme's soul, a proof assistant's spine, grown from one spore.

programming-language rust algebraic-effects dependent-types compiler functional-programming llvm webassembly proof-assistant type-theory cubical-type-theory self-hosting interactive-theorem-proving theorem-prover programming-language-theory effect-handlers normalization-by-evaluation quantitative-type-theory
  • Updated Jul 9, 2026
  • Rust

Add this topic to your repo

To associate your repository with the quantitative-type-theory topic, visit your repo's landing page and select "manage topics."

Learn more