type-theory
There are 206 repositories under type-theory topic.
steshaw/plt
Programming Language Theory λΠ
HigherOrderCO/Kind1
A next-gen functional language
sdiehl/write-you-a-haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
leanprover/lean3
Lean Theorem Prover
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
pikelet-lang/pikelet
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
eashanhatti/peridot
A fast functional language based on two level type theory
rntz/datafun
Research on integrating datalog & lambda calculus via monotonicity types
typedefs/typedefs
Programming language agnostic type construction language based on polynomials.
stepchowfun/proofs
My personal repository of formally verified mathematics.
RedPRL/sml-redprl
The People's Refinement Logic
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
lazear/types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
paarthenon/variant
Variant types in TypeScript
ditto/ditto
A Super Kawaii Dependently Typed Programming Language
err0r500/foundational-knowledge-for-programmers
List of resources about foundational knowledge for programmers (supposed to last a few decades)
advancedresearch/path_semantics
A research project in path semantics, a re-interpretation of functions for expressing mathematics
cicada-lang/cicada-solo
Cicada Language (solo version)
ilya-klyuchnikov/ttlite
A SuperCompiler for Martin-Löf's Type Theory
owo-lang/minitt-rs
Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
owo-lang/voile-rs
Dependently-typed row-polymorphic programming language, evolved from minitt-rs
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
brendanzab/rust-nbe-for-mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
TheoWinterhalter/formal-type-theory
Formalising Type Theory in a modular way for translations between type theories
owo-lang/narc-rs
(WIP) Dependently-typed programming language with Agda style dependent pattern matching
bor0/gidti
Book: Introduction to Dependent Types with Idris
molikto/mlang
Towards changing things and see if it proofs
madnight/awesome-category-theory
A curated list of awesome Category Theory resources.
ice1000/guest0x0
Neon lights in the night tonight and stars that shine in the open sky
jbrkr/Category_Theory_Natural_Language_Processing_NLP
List of papers and other resources at the intersection of Category Theory and NLP.
mr-ohman/logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda