An analysis tool for Python that blurs the line between testing and type systems.
A garden of small programming language implementations 🪴
Tiny ML, Rust types, and category theory, executable structure, not AI magic.
Reproduction Package for the paper "Type-Constrained Code Generation with Language Models" [PLDI 2025]
Playing with type systems
A collection of programming languages and type systems.
C++ Implementations of programming languages and type systems studied in "Types and Programming Languages" by Benjamin C. Pierce..
Hindley–Milner type inference implemented in Python.
OCaml inspired language
The Agda mechanization of a gradual security-typed programming language with general mutable references.
Type system workshop for reactathon
Demo code showing off the new true exhaustiveness checks with Python 3.10 + Pyright
Experimental language for exploring scoped effects, named scopes, and coeffects
TLC SRC — The software industry is broken — let's reboot the industry instead of our programs!
Naming is programming. Renaming a field changes what the model computes. Alpha equivalence breaks when the compilation target reads natural language.
Resource-safe, effect-typed programs in syntax you already know. A checked affine core with familiar Faces — JavaScript-, Python-, functional-, and pseudocode-shaped surfaces — compiling to typed WebAssembly.
Python-syntax AffineScript — write Python-style code, get affine resource guarantees and typed WASM
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.
A tool for defining categorical structures and automatically deriving their internal type theories, proof systems, and interpreters. Specify a category, get a programming language.
Agent IR — a compilation infrastructure for agentic systems: a typed, verifiable IR whose effect and capability system makes agent optimizations decidable rather than heuristic, and crash recovery sound. Specification plus a Rust reference implementation.
To associate your repository with the type-systems topic, visit your repo's landing page and select "manage topics."