An introductory course to Homotopy Type Theory

A formalization of geometry in Coq based on Tarski's axiom system

The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.

Formalising Type Theory in a modular way for translations between type theories

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

Formalization of the polymorphic lambda calculus and its parametricity theorem

Deciding Presburger arithmetic in agda

Two-Level Type Theory

🧊 An indexed construction of semi-simplicial and semi-cubical types

The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.

Official repository of the Autosubst 2 project.

Linear algebra formalization in Agda

Formalization of Categories with Families

Formalization of some elementary mathematical theories in Coq

Formal Verification of Telegram's MTProto 2.0

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

A Coq formalisation of the R programming language

Formalization of termination of Gödel's System T