#

formalization

Here are 57 public repositories matching this topic...

EgbertRijke / HoTT-Intro

An introductory course to Homotopy Type Theory

book coq mathematics agda formalization hott univalence

Updated Jul 24, 2020
Agda

GeoCoq / GeoCoq

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

geometry euclid coq formalization elements archimedes tarski-axiom hilbert-axioms desargues pappus parallel-postulate continuity

Updated Nov 30, 2021
Coq

TheoWinterhalter / formal-type-theory

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

reflection type-theory formalization

Updated Jan 10, 2018
Coq

mgree / smoosh

Open

Tool for just debugging ASTs

mgree commented Oct 27, 2021

Shtepper is too verbose.

Read more

enhancement good first issue

Open

Parser tests?

Open

Implement other operations for arithmetic expansion

Find more good first issues

gallais / agda-presburger

Deciding Presburger arithmetic in agda

agda formalization decision-procedure presburger-arithmetic

Updated Dec 23, 2019
Agda

annenkov / two-level

Two-Level Type Theory

proof-assistant type-theory lean formalization homotopy-type-theory

Updated Dec 13, 2019
Lean

jonsterling / coq-guarded-computational-type-theory

Sponsor

dependent-types formalization guarded-recursion

Updated Apr 15, 2018
Coq

Lysxia / system-F

Formalization of the polymorphic lambda calculus and its parametricity theorem

lambda-calculus coq formalization polymorphism denotational-semantics system-f parametricity

Updated May 2, 2019
Coq

ualib.github.io

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.

dependent-types logic agda formalization agda-library universal-algebra typetheory agda-ualib

Updated Dec 8, 2021
TeX

ivashkev / math-formalizations

Formalization of some elementary mathematical theories in Coq

geometry euclid coq formalization elements hilbert-axioms

Updated Mar 29, 2020
Coq

artagnon / bonak

🧊 An iterated Grothendieck construction of semi-cubical types

paper cubical-type-theory formalization research-project

Updated Apr 5, 2022
TeX

superhaNds / cwfs

Formalization of Categories with Families

lambda-calculus agda formalization

Updated Oct 4, 2021
Agda

felko / linear-algebra

Linear algebra formalization in Agda

linear-algebra agda formalization agda-library

Updated Nov 28, 2019
Agda

uds-psl / autosubst2

Official repository of the Autosubst 2 project.

coq formalization metatheory-language

Updated Jan 3, 2022
Haskell

jonsterling / agda-effectful-forcing

Sponsor

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.

type-theory formalization intuitionism system-t bar-induction

Updated Sep 22, 2020
Agda

miculan / telegram-mtproto2-verification

Formal Verification of Telegram's MTProto 2.0

formalization proverif cryptographic-protocols

Updated Jan 2, 2022
Shell

tchajed / goedel-t

Formalization of termination of Gödel's System T

coq formalization

Updated Jun 6, 2021
Coq

ajrouvoet / implicits.agda

Mechanized formalization of Implicit resolution in Agda

proof agda formalization pts implicits

Updated Jun 28, 2017
Agda

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.

dependent-types logic theorem-proving mathematics verification type-theory set-theory data-structures category-theory agda formalization proofs mathematics-library

Updated Apr 16, 2021
Agda

Mbodin / CoqR

A Coq formalisation of the R programming language

r rstats coq-formalization formalization

Updated Apr 8, 2022
R

Lysxia / coq-mtl

Formalized laws for mtl

haskell coq effects monad formalization monad-transformers laws

Updated Oct 20, 2019
Coq

marco10507 / formalization-of-sorting-algorithms

some sorting algorithms' formalisation

mergesort insertion-sort selection formalization isabelle-hol

Updated Aug 17, 2019
Isabelle

radeusgd / QuotedPatternMatchingProof

A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.

scala lambda-calculus coq formalization dotty

Updated Jul 23, 2020
TeX

zchn / eth-acl2

An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.

ethereum verification formal-methods formalization proofs evm acl2

Updated Jul 31, 2018
Common Lisp

vitalsong / bastard

more than just a package manager

git toml cmake generator cross-platform cpp project-template cargo build-tool formalization git-hooks clang-format dependencies lockfile

Updated Mar 14, 2022
CMake

harp-project / Core-Erlang-Formalization

coq formalization core-erlang

Updated Apr 7, 2022
Coq

co-dan / BI-cutelim

Cut elimination for the logic of Bunched Implications (BI), and some extensions.

coq logic formalization metatheory

Updated Dec 9, 2021
Coq

cogumbreiro / habanero-coq

Coq formalization of the Habanero programming model.

synchronization phaser coq parallel-computing coq-formalization formalization formal-verification async-finish habanero-coq

Updated May 7, 2018
Coq

capital-G / xenakis-workgroup

Material created during the Iannis Xenakis workgroup

music-composition stochastic formalization music-informatics

Updated Dec 5, 2021
Jupyter Notebook

ggt

zampino / ggt

A random collection of Agda facts around the Theory of Group Actions

agda formalization group-theory group-actions

Updated Oct 18, 2020
Agda

Improve this page

Add a description, image, and links to the formalization topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the formalization topic, visit your repo's landing page and select "manage topics."