Programming Language Theory λΠ
-
Updated
Dec 2, 2024 - CSS
#
type-theory
Here are 230 public repositories matching this topic...
A modern proof language
dependent-types functional-programming lambda-calculus type-theory theorem-prover formality moonad proof-language proof-languages
-
Updated
Jan 22, 2025 - Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
compiler functional-programming book lambda-calculus evaluation type-theory type pdf-book type-checking haskel type-system functional-language hindley-milner type-inference intermediate-representation
-
Updated
Jan 11, 2021 - Haskell
Agda is a dependently typed programming language / interactive theorem prover.
-
Updated
Jun 20, 2025 - Haskell
Lean Theorem Prover
-
Updated
Oct 14, 2023 - C++
A Coq library for Homotopy Type Theory
-
Updated
Jun 16, 2025 - Rocq Prover
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
programming-language rust typechecker dependent-types compiler type-theory systems-language type-system systems-programming bidirectional-typechecking dependent-record-types dependent-records
-
Updated
May 16, 2021 - Rust
Experimental implementation of Cubical Type Theory
-
Updated
Sep 21, 2023 - Haskell
Playing Sudoku in TypeScript while the type checker highlights mistakes.
-
Updated
Aug 20, 2024 - TypeScript
Research on integrating datalog & lambda calculus via monotonicity types
-
Updated
Jun 21, 2022 - TeX
A fast functional language based on two level type theory
-
Updated
Jan 6, 2023 - Haskell
Programming language agnostic type construction language based on polynomials.
serialization types marshalling type-theory category-theory serialization-library f-algebras type-definitions
-
Updated
May 29, 2024 - Idris
My personal repository of formally verified mathematics.
-
Updated
Mar 20, 2025 - Coq
A garden of small programming language implementations 🪴
dependent-types interpreter type-theory programming-languages compilers type-checking l-systems interpreters elaboration compilation typechecking normalization-by-evaluation semantic-typechecking type-systems language-garden
-
Updated
Jun 20, 2025 - OCaml
Logical manifestations of topological concepts, and other things, via the univalent point of view.
type-theory agda ordinal homotopy-type-theory univalent-foundations constructive-mathematics compact-type totally-separated-type injective-type searchable-set univalent-mathematics
-
Updated
Jun 20, 2025 - Agda
The People's Refinement Logic
-
Updated
Jan 1, 2023 - Standard ML
Lecture notes on univalent foundations of mathematics with Agda
dependent-types type-theory agda lecture-notes mltt homotopy-type-theory univalent-foundations univalent-mathematics hott-uf martin-lof-type-theory univalence-axiom function-extensionality propositional-truncation univalent-type-theory
-
Updated
Apr 16, 2024 - Agda
😎TT
-
Updated
Oct 21, 2023 - OCaml
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
-
Updated
Mar 25, 2022 - OCaml
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
-
Updated
Jul 26, 2020 - Rust
Improve this page
Add a description, image, and links to the type-theory topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the type-theory topic, visit your repo's landing page and select "manage topics."