Verified Lambda Interpreter and Concurrent Parallel Matrix Runtime. Joe, Bob, and Alice languages share the same Standard ML like BNF grammar.
Joe
Joe is a certified bytecode stack interpreter and Intel/ARM code compiler.
[1] — MinCaml
[2] — CoqASM
[3] — Verified LISP Interpreter
[4] — Kind
Bob
Bob is a parallel concurrent non-blocking zero-copy run-time with CAS cursors [4,5].
[5] — Kernel
[6] — Pony
[7] — Erlang
Alice
Alice is a linear types calculus with partial fractions [6] for BLAS level 3 programming.
[8] — NumLin
Sound and Consistent Predicative Formal Languages. Alonzo, Henk, Per, Anders languages share the same Lean like BNF grammar.
Alonzo
Alonzo is an STLC-40 type system as example of core calculus discovered before fibrational ΠΣ provers.
STLC-40 — Simple Theory of Types
Henk
Henk is a Pure Type System (PTS-91) in the style of Coquand/Huet Calculus of Inductive Constructions (CoC-88) with infinite numbere of universes. Henk also supports AUTOMATH syntax (AUT-68).
AUT-68 — AUTOMATH
CoC-88 — Calculus of Constructions
PTS-91 — Pure Type System (Π)
Per
Per is a ΠΣ (MLTT-72) prover with Calculus of Inductive Constructions and idenitity types (MLTT-75). The natural extension of CoC to CIC was done by Frank Pfenning and Christine Paulin (IND-89).
Mini-TT — OCaml implementation
MLTT-72 — Pi, Sigma
MLTT-75 — Pi, Sigma, Id
MLTT-80 — 0, 1, 2, W, Pi, Sigma, Id
PP-89 — Inductively Defined Types
CIC-2015 — Calculus of Inductive Constructiions
Anders
Anders is a Homotopy Type System (HTS-2013) with Strict Equality and Cubical Agda (CCHM-2016) primitives.
HTS-2013 — Homotopy Type System
BCH-2014 — Cubical Sets
CCHM-2015 — Cubical Type System
OP-2016 — Topos Axioms
CHM-2017 — Huber Equations
VMA-2017 — Cubical Agda
Urs
Urs is an equivariant superhomotopy type system with fermion and boson modalities built-in into type checker.
R-HoTT — Rezk Infinity Categories
G-HoTT — Guarded Cubical
L-HoTT — Linear HoTT
ES-HoTT — Equivariant Super HoTT