Cicada Language (PLCT little team)

Cicada Language (solo version)

Logical relation for predicative CC omega with booleans and an intensional identity type

A simple scala-like dependent type programming language

Anders: Cubical Type Checker

A dependent type theory logic for Isabelle

Type-checking and type-inference for a spartan dependent type theory.

A dependently typed programming language embedded in JSON, that can be used as a schema checker for JSON data.

Introduction to typelevel programming: phantom types, dependent types, path dependent types and Curry-Howard isomorphism.

A dependently typed programming language

Dependently typed lambda calculus - A Simple Proof Assistant

The Agda Universal Algebra Library (html docs available at the url below)

A programming language based on extensional Martin Lof Type Theory

Hurricane: HoTT-I Type System