This repository contains various different very incomplete mechanizations of Luo's Extended Calculus of Constructions, usually with a few additions:
- Local definitions (let expressions), with or without type annotations
- Booleans with dependent conditionals (elimination)
- Polymorphic universes (Redex only)
Beluga is an LF-like proof assistant using contextual type theory to implement higher-order abstract syntax. An installation guide can be found here, and a reference manual here.
The Beluga model has reduction, conversion, equivalence, subtyping, and typing relations. An attempt at proving subject reduction was made.
Redex is a Racket library for modelling languages with binding, reduction relations, and judgements. The reference can be found here.
The Redex model implements type synthesis for ECC with universe polymorphism and anonymous universes using an algorithm from Type Checking with Universes. The constraint-checker is incredibly inefficient and not yet actually used in the type synthesis algorithm. The paper doesn't specify how relationships between concrete type levels (i.e. naturals) should be enforced, so at the moment, for every pair of naturals (i, j), if (i < j), then we add this edge to the graph. Much testing remains to be done.
Idris is a general-purpose dependently-typed language based on quantitative type theory, with support for writing proofs. This repo uses Idris 2, whose documentation can be found here. The Idris 1 documentation is helpful as well. The installation guide for Idris 2 is here.
The Idris model implements variables using a locally-nameless shifted-names scope-safe representation. That is, bound variables are implemented using de Bruijn levels, the levels are never greater than the binding depth, and free variables are implemented using names with indices to avoid collision. The shifted-names implementation is complete, but lacks proofs of all its properties, which may be translated from the Coq implementation at some point.