Skip to content

groupoid/groupoid.space

Repository files navigation

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