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