groupoid

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