Groupoid Infinity

Groupoid Infinity is building integrated environment for mathematician:

* ANT — Publishing environment a la ТеХ
* CAS — Computable and Symbolic Mathematics a la Wolfram Mathematica
* NOTE — Notebook Interface a la Jupyter
* RUN — Runtime Interpreter and Virtual Machines
* VERIFY — Theorem Prover a la Lean/Agda

RUN: Virtual Machines and Runtime Languages

* APL — persistent tensor array processing runtime (get, put, fold)
* CPS — fast certified L1 lambda CPS interpreter as runtime (fun, app)
* EFF — effect type system for (in)finite I/O (getString, putString, pure)
* PRO — intercore protocol for process calculus (spawn, send, recv)
* N2O — app frameworks: MNESIA, BPE, N2O, KVS, NITRO

VERIFY: Verification Languages

* STLC — Simply Typed Lambda Calculus
* PTS — Pure Type System for encodings exploration
* HTS — Modal CCHM Homotopy Type System for math modeling
* HoTT-I — Arend-like core