formalization

GeoCoq/GeoCoq

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

mgree/smoosh

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

TheoWinterhalter/formal-type-theory

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

loganrjmurphy/LeanEuclid

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

Lysxia/system-F

Formalization of the polymorphic lambda calculus and its parametricity theorem

gallais/agda-presburger

Deciding Presburger arithmetic in agda

annenkov/two-level

Two-Level Type Theory

artagnon/bonak

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

jonsterling/coq-guarded-computational-type-theory

ualib/ualib.github.io

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.

uds-psl/autosubst2

Official repository of the Autosubst 2 project.

ivashkev/math-formalizations

Formalization of some elementary mathematical theories in Coq

superhaNds/cwfs

Formalization of Categories with Families

felko/linear-algebra

Linear algebra formalization in Agda

jonsterling/agda-effectful-forcing

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.

miculan/telegram-mtproto2-verification

Formal Verification of Telegram's MTProto 2.0

harp-project/Core-Erlang-Formalization

Mbodin/CoqR

A Coq formalisation of the R programming language

tchajed/goedel-t

Formalization of termination of Gödel's System T

Lolirofle/stuff-in-agda

Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

siraben/coq-wigderson

Formalization of Wigderson's graph coloring algorithm in Coq

capital-G/xenakis-workgroup

Material created during the Iannis Xenakis workgroup

Lysxia/coq-mtl

Formalized laws for mtl

ajrouvoet/implicits.agda

Mechanized formalization of Implicit resolution in Agda

choukh/agda-lvo

large veblen ordinal in agda

marco10507/formalization-of-sorting-algorithms

some sorting algorithms' formalisation

cogumbreiro/habanero-coq

Coq formalization of the Habanero programming model.

matematiflo/CompAssistedMath2024

GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.

pitmonticone/FLT3

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

thery/minirubik

Solving the mini Rubik (2x2) in Coq

vitalsong/bastard

more than just a package manager

Gradual-Typing/LambdaIFCStar

The Agda mechanization of a gradual security-typed programming language with general mutable references.

jeffreybakker/wsn

Calculating the Risk of Valve Failures when Maintaining Water Supply Networks

jjaassoonn/flat

Equivalent definitions of flatness

snow0815/tribAIn

tribAin - ontology for scientific experiments in the domain of tribology