Groupoid Infinity is doing research in type theory, model encodings, programs extraction and formalization of mathematics. We believe in high performance certified virtual machines, where certified programs extracted from provers should run on. We also want to use group theory and homotopy theory for proving properties about these programs.

Languages

Non-dependent languages are targets or runtimes, and dependently typed language are provers.

Runtimes

Groupoid Infinity runtimes and effect type systems.

31 DEC 2016 — Certified CPS Interpreter
31 DEC 2016 — Intercore SMP Protocol
10 OCT 2016 — Array Processing
10 OCT 2016 — Effect Type System
24 MAY 2018 — Process Type System

Provers

Groupoid Infinity provers for logic, lambda encodings exploration and homotopy calculus.

10 OCT 2016 — Pure Type System
6 JUL 2018 — Homotopy Type System
19 JAN 2020 — Principia System

Models

Great language should comes with a great library.

3 AUG 2018 — Formal Mathematics

Foundation

The examples of HTS base library man pages.

16 JUL 2017 — Pi, Sigma, Path, Proto, Prop, Stream, List, Nat, Maybe, IO, IOI, Bool

Mathematics

The series of notes on Homotopy Theory, Category Theory, Topos Theory, Sheaf Theory and Differential Geometry, formalized in HTS.

10 OCT 2017 — Isomorphism
19 OCT 2017 — Inductive Data Types
20 JUN 2017 — Hopf Fibrations
5 NOV 2017 — Category
20 MAY 2018 — Bundle
25 JUL 2018 — CW Complex
9 AUG 2018 — Formal Set Topos
30 DEC 2018 — Equivalence
13 JAN 2019 — Presheaf Type Theories
15 JAN 2019 — Homotopy Limits
15 JAN 2019 — Differential Geometry
17 JAN 2019 — de Rham Cohesion
22 JAN 2019 — Homology

Articles

The series of articles on foundation and mathematics of Homotopy Type Theory.

Issue I: Internalizing MLTT
Issue III: Homotopy Type Theory
Issue VIII: Formal Set Topos
Addendum I: Pure Type System
Addendum II: Many Faces of Equality