AXIO/X

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


fun a (0, n) = n + 1
  | a (m, 0) = a (m - 1, 1)
  | a (m, n) = a (m - 1, a (m, n - 1))

Bob

Bob is a parallel concurrent non-blocking zero-copy run-time with CAS cursors [4,5].

[5] — Kernel
[6] — Pony
[7] — Erlang


fun proc =
let val p0 = pub(0,8)
    val s1 = sub(0,p0)
    val s2 = sub(0,p0)
 in send(p0,11);
    send(p0,12);
    [ receive(s1);
      receive(s2);
      receive(s1);
      receive(s2)
    ]
    end

Alice

Alice is a linear types calculus with partial fractions [6] for BLAS level 3 programming.

[8] — NumLin


fun simpleConvolution (i n: int) (x0: float) (write w: vector float)
  : vector float
  = begin
      if n = i then result.emit(write),
      a = [w0,w1,w2] = w.get(0,3),
      b = [x0,x1,x2] = [ x0 | write.get(i,2) ],
      write.set(i, Dotp(a,b)),
      simpleConvolution((i + 1),n,x1,write,w)
    end

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


def zero : (T → T) → T → T := λ (s: T → T) (z: T), z
def succ : ((T → T) → T → T) → ((T → T) → T → T)
 := λ (w: (T → T) → T → T) (y: T → T) (x: T), y (w y x)

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 (Π)


def N := Π (A : U), (A → A) → A → A
def zero : N := λ (A : U) (S : A → A) (Z : A), Z
def succ : N -> N := λ (n : N) (A : U) (S : A → A) (Z : A), S (n A S Z)
def plus (m n : N) : N := λ (A : U) (S : A → A) (Z : A), m A S (n A S Z)
def mult (m n : N) : N := λ (A : U) (S : A → A) (Z : A), m A (n A S) Z
def pow (m n : N) : N := λ (A : U) (S : A → A) (Z : A), n (A → A) (m A) S Z

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


def empty      : U := inductive { }
def L¹ (A : U) : U := inductive { nil | cons (head: A) (tail: L¹ A) }
def S¹         : U := inductive { base | loop : Equ S¹ base base }

def quot (A: U) (R : A -> A -> U) : U
 := inductive { quotient (a: A)
              | identification (a b: A) (r: R a b)
              : Equ (quot A R) (quotient a) (quotient b)
              }

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


def idfun  (A : U) : A → A := λ (a : A), a
def idfun′ (A : U) : A → A := transp (<i> A) 0
def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a
def isFiberBundle (B: U) (p: B → U) (F: U): U
 := Σ (v: U) (w: surjective v B), (Π (x: v), PathP (<_>U) (p (w.1 x)) F)
def ~~ (X : U) (a x′ : X) : U := Path (ℑ X) (ι X a) (ι X x′)
def 𝔻 (X : U) (a : X) : U := Σ (x′ : X), ~~ X a x′
def unitDisc (X : U) (x : ℑ X) : U := Σ (x′ : X), Path (ℑ X) x (ι X x′)
def starDisc (X : U) (x : X) : 𝔻 X x := (x, idp (ℑ X) (ι X x))
def T∞ (A : U) : U := Σ (a : A), 𝔻 A a
def inf-prox-ap (X Y : U) (f : X → Y) (x x′ : X) (p : ~~ X x x′)
  : ~~ Y (f x) (f x′) := <i> ℑ-app X Y f (p @ i)
def d (X Y : U) (f : X → Y) (x : X) (ε : 𝔻 X x) : 𝔻 Y (f x)
 := (f ε.1, inf-prox-ap X Y f x ε.1 ε.2)
def T∞-map (X Y : U) (f : X → Y) (τ : T∞ X) : T∞ Y
 := (f τ.1, d X Y f τ.1 τ.2)
def is-homogeneous (A : U)
 := Σ (e : A) (t : A → equiv A A),
    Π (x : A), Path A ((t x).1 e) x

Dan

Dan is a simplicial CCHM-based verification system with Simplicial, Simplex, Chain, Monoid, Category, Group primitives built into the type checker core. Dan is new Rzk/GAP replacement.

R-HoTT — Rezk Infinity Categories
Hopf-HoTT — Hopf Fibrations, Stable Spherical Homotopy Groups


def path_z2_category : Category
 := П (x y : Simplex),
      (f g h : Simplex),
      (z2 : Group(П (e a : Simplex), a² = e ⊢ 1 (a | a² = e))),
      f ∘ g = h
    ⊢ 2 (x y | f g h | f ∘ g = h)

def z3 : Group
 := П (e a : Simplex),
      a³ = e
    ⊢ 1 (a | a³ = e)

def Möbius : Simplex
 := П (a b c : Simplex),
      (bc ac : Simplex), ab = bc ∘ ac
    ⊢ 2 (a b c | bc ac ab)

Élie

Élie is a CCHM-based verification system with Hopf Primitives primitives built into the type checker core.

Hopf-HoTT — Hopf Fibrations, Stable Spherical Homotopy Groups

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