type-theory
There are 210 repositories under type-theory topic.
steshaw/plt
Programming Language Theory λΠ
HigherOrderCO/Kind1
A modern proof 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
gruhn/typescript-sudoku
Playing Sudoku in TypeScript while the type checker highlights mistakes.
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/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
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
veyselusta/programming-language-research
Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.
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
brendanzab/rust-nbe-for-mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
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
madnight/awesome-category-theory
A curated list of awesome Category Theory resources.
molikto/mlang
Towards changing things and see if it proofs
jbrkr/Category_Theory_Natural_Language_Processing_NLP
List of papers and other resources at the intersection of Category Theory and NLP.