Dependent types ​

Magmide, TeenyTT & Kind look interesting.

How to implement dependent types in 80 lines of code is good read.

Elaboration Zoo has great dependent type checker implementations.

Links ​

• Cubical Adventures
• Resources for "The Little Typer" study group
• Compiling with Dependent Types (Thesis PDF)
• Live Functional Programming with Typed Holes (2019)
• Silt - An in-progress fast, dependently typed, functional programming language implemented in Swift.
• Minimal implementations for dependent type checking and elaboration
• Remora - Dependently-typed language with Iverson-style implicit lifting.
• Juvix - High-level programming language for writing privacy preserving apps. (Reddit)
• sixty - Dependent type checker using normalisation by evaluation.
• Formality - Efficient dependently-typed systems programming language and proof assistant. (HN)
• Certified Programming with Dependent types (PDF) (Code)
• voile-rs - Dependently-typed programming language with a non-dependent version of row-polymorphism, meta variable resolution and implicit parameter syntax.
• Approximate Normalization for Gradual Dependent Types (2019)
• A Dependently Typed Language (2019)
• Pi-Forall language - Demo implementation of a simple dependently-typed language.
• Dependent types, Vitaly Bragilevsky (2020)
• Next 700 Module Systems - Extending Dependently-Typed Languages to Implement Module System Features In The Core Language.
• A Dependently Typed Multi-Stage Calculus (2019)
• Dependent Type Systems as Macros (2019)
• In Further Praise of Dependent Types (2020) (HN)
• Checking Dependent Types with Normalization by Evaluation: A Tutorial
• Epigram: Practical Programming with Dependent Types (2004) (Lobsters)
• A Tutorial Implementation of a Dependently Typed Lambda Calculus (PDF)
• How to implement dependent type theory (2012)
• Dependently-typed compilers don't go wrong (2020)
• Dependable Types explained in parts (2018)
• Research library of the ##dependent IRC channel
• Epigram language - Dependently typed programming language and an interactive programming environment. (Code)
• A dependently typed calculus with pattern matching and erasure inference (2020)
• A general definition of dependent type theories (2020)
• dreamtt - Pedagogic implementation of abstract bidirectional elaboration for dependent type theory.
• Metagen - Dependently type-safe code generator.
• Gradual Dependently Typed Language
• Dependent types to code are what static types to data (2020)
• Pie language - Little Language with Dependent Types. Companion language for The Little Typer book.
• What makes dependent type theory more suitable than set theory for proof assistants? (HN)
• Dependent types at work (2009) (Code)
• curnelo - Cur dependently-typed programming language, implemented in miniKanren.
• cur - Language with static dependent-types and dynamic types, type annotations and parentheses, theorem proving and meta-programming.
• Daniel Gratzer Research
• Improving Error Messages for Dependent Types with Constraint-based Unification (2016) (Code)
• Dependently Typed Linear π-Calculus in Agda
• Type systems for programs respecting dimensions (2021)
• Calculating Dependently-Typed Compilers (2021)
• A Dependently Typed Assembly Language
• Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version) (2019)
• Durin - Dependent Unboxed higher-oRder Intermediate Notation.
• Pika - Small, dependently typed ML with algebraic effects and unboxed types.
• Clamn - Functional systems language leveraging dependent types, partial evaluation, and data layout abstraction.
• TTstar - Dependently typed core calculus with erasure inference.
• staged - Experimental staged language with dependent types.
• dfuzz - Linear Dependent Types for Differential Privacy.
• datatt - Implementation of a dependent type theory with user defined datatypes.
• Pompom - Dependently typed language for proofs that you can implement in one day. (HN)
• Specification for Dependent Types in Haskell (Core)
• (2) Program Adverbs: Structures for Embedding Effectful Programs (2021)
• Dependent Object Types (DOT) - Formalization of the Dependent Object Types (DOT) calculus.
• Magma - Dependently-typed language. (Lobsters) (My Path to Magma (2021))
• Formal Metatheory of Second-Order Abstract Syntax
• Aya - Programming language and a proof assistant designed for formalizing math and type-directed programming. (Web)
• tinka-hs - Dependently typed programming language written in Haskell.
• Cedille - Dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations. (Web)
• Mini-TT - Curricula for learning how to implement dependently typed languages by recursive paper-chasing.
• MiniJuvix - Dependently functional programming language for writing efficient formally-verified validity predicates, which can be deployed to various distributed ledgers.
• FormCoreJS - Minimal pure functional language based on self dependent types.
• Dependently typed programming with finite sets (Code)
• Castle Bravo: Experimental HoTT Implementation
• Magmide - Dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
• TeenyTT - Small, didactic proof assistant designed around dependent type theory.
• pistachio - Small, nutty dependently typed language.
• Tutorial implementation on an elaborator of a dependently typed language with pruning
• Using dependent types to write proofs in Haskell (2021)
• Mini Yu - Dependently typed programming language prototype.
• How to implement dependent types in 80 lines of code (Lobsters)
• Dependently Typing R Vectors, Arrays, and Matrices (2023) (HN)
• algaett - Experimental elaborator for dependent type theory using effects and handlers.