AXIO

8.0


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

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