**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