Groupoid Infinity

Groupoid Infinity is building integrated environment for mathematician:

1. RT — Runtime Interpreters and Virtual Machines
2. CAS — Computable and Symbolic Mathematics a la Wolfram Mathematica, GAP
3. CERT — Theorem Prover a la Lean/Agda
4. ANT — Publishing environment a la ТеХ
5. NOTE — Notebook Interface a la Jupyter, GUI

CAS: Computer Algebra System

• GAP — Groups Algorithm Programming
• FTL — Formal Tensor Language

RT: Virtual Machines and Runtime Languages

• CPS — Certified Interpreter
• EFF — Effects IOI, IO
• FTL — Formal Tensor Language
• PRO — Intercore Protocol for Pi-calculus (spawn, send, recv)
• N2O — App frameworks: MNESIA, BPE, N2O, KVS, NITRO

CERT: Verification Languages

• STLC — Simply Typed Lambda Calculus
• PTS — Pure Type System for encodings exploration
• HTS — Modal CCHM Homotopy Type System for math modeling