Infinity Language

AST Specification as Inductive Constructions

The idea of Infinity Langauge came from the needs of unification and arranging different calculuses as an extensions to the core of the language with dependent types (or MLTT core). While been working on distributed systems, data storages and stream processing, the core two languages: pi calculus and stream calculus discovered to be connected and being driven by a language with quantifiers as a primitives.

Infinity is a dependently typed language for stream processing, distributed processing and text processing. We use Coq to prototype the standard library including the theories needed to be able to prove code invariants instead of testing them. Infinity is a source to source translator that lets you use different languages at runtime: Erlang, Rust, Clang, Futhark, Julia, etc.

Infinity language presents a solid and unified way of modeling inter-language computations and inter-system communications within a single language with compact core. We strive for utilizing parallel hardware such as GPU and SSE/AVX SIMD instructions and providing a robust and verified distributed environment with process and channels runtime.

Inf Language is built on top of CoC pure type system, predicative universes and inductive constructions you may find in other MLTT provers like Lean, Coq, Idris, Agda, and F*. As algebraїс prover, Inf supports data and record polynomial functors as fundamental language constructions implemented in a form of hygienic macros over the AST. Everything in Infinity Language is encoded as inductive construction: from the equality property up to process calculus. Both Infinity language and its macrosystem are built using AST types, described in this document.

Language Extensions

Require Import core. Require Import homotopy. Require Import pi. Require Import stream. Require Import effect. Inductive MLTT := Pi: MLTT -> MLTT -> MLTT | Lam: Binder -> MLTT -> MLTT | App: MLTT -> MLTT -> MLTT | Sigma: MLTT -> MLTT -> MLTT | Pair: MLTT -> MLTT -> MLTT | Fst: MLTT -> MLTT | Snd: MLTT -> MLTT | Where: MLTT -> Decls -> MLTT | Var: Ident -> MLTT | U: MLTT | Con: Label -> list MLTT -> MLTT | Split: Loc -> list Branch -> MLTT | Sum: Binder -> NamedSum -> MLTT | HIT: HomotopyCalculus -> MLTT | PI: PiCalculus -> MLTT | EFF: EffectCalculus -> MLTT | STREAM: StreamCalculus -> MLTT.

Compiler Passes

  1. INF — Macro Expansion
  2. NORMAL — Typechecking
  3. ERASE — Type Information Erasure
  4. EXTRACT — Extract VM Lambda


The type system is completely described by the PTS SAR notation, given by Barendregt. Find more info in Axioms and Inference Rules of underlying Om intermediate language.

record PTS: * := (S: ∀ (n: nat) → star n) (A: ∀ (i: nat) → type i (succ i)) (R: ∀ (i: nat) → ∀ (j: nat) → pi i j (max i j))



Om language is the macrosystem terminal language. Language forms of pure Macro or inpure Effect types are expanded to the terminal language. For the details please refer to the Om Assembler description.

data Om: * := (star: Star → Om) (var: Var → Om) (app: App → Om) (arrow: Arrow → Om) (pi: Pi → Om)


record Star: * := (index: nat)


record Var: * := (name: string)

Arrow / Pi

record Arrow Pi: * := (name: string) (arg: Om) (body: Om)


record App: * := (fun: Om) (arg: Om)


Macro language subsystem is the core of Inf language and dedicated to compile the prelude desceibed in the Core Types document. Om language is the target language of macroexpansions of data and record inductive constructions, let construction and univariable case pattern matching.

data Macro: * := (record: Record → Macro) (data: Data → Macro) (let: Let → Macro) (case: Case → Macro)

Case / Receive

record Case Receive: * := (of: Inf) (legs: list (prod atom (prod Om Inf))) (default: Inf)


record Let: * := (binds: list (prod string Inf)) (in: Inf)

Record / Data

record Record Data: * := (name: string) (base: Om) (body: list (prod string Inf))


Effect syntax extensions defined basic process calculus axioms, IO and exception handling.

data Effect: * := (receive: Receive → Effect) (spawn: Spawn → Effect) (send: Send → Effect) (try: Exception → Effect) (raise: Exception → Effect) (write: File → Effect) (read: File → Effect)


record Process: (Sigma: *) → (X: *) → * := (action: Sigma → X → GenServer X)


record Spawn: (proc: Process) (raise: list Eff)


record Send: (Sigma: *) → * := (message: Sigma) (to: Process Sigma)


  1. Om archives.
  2. Inf archives.
  3. Git sources.
  4. Inf git sources.