| title |
|---|
Dependent types |
Magmide & TeenyTT look interesting.
- 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 - More elegant language for a more civilized age. (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