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.

session-types proof-engineering verified-compiler linear-types type-systems programming-language-design affine-types mechanized-metatheory quantitative-type-theory
  • Updated Aug 7, 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

Improve this page

Add a description, image, and links to the quantitative-type-theory topic page so that developers can more easily learn about it.

Curate this topic

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