An introductory course to Homotopy Type Theory
-
Updated
Jul 24, 2020 - Agda
#
formalization
Here are 45 public repositories matching this topic...
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
Oct 23, 2020 - Coq
Formalising Type Theory in a modular way for translations between type theories
-
Updated
Jan 10, 2018 - Coq
Deciding Presburger arithmetic in agda
-
Updated
Dec 23, 2019 - Agda
Formalization of the polymorphic lambda calculus and its parametricity theorem
-
Updated
May 2, 2019 - Coq
-
Updated
Apr 15, 2018 - Coq
Linear algebra formalization in Agda
-
Updated
Nov 28, 2019 - Agda
Two-Level Type Theory
-
Updated
Dec 13, 2019 - Lean
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.
-
Updated
Sep 22, 2020 - Agda
Formalization of some elementary mathematical theories in Coq
-
Updated
Mar 29, 2020 - Coq
Formalization of Categories with Families
-
Updated
Oct 28, 2018 - Agda
Formalized laws for mtl
-
Updated
Oct 20, 2019 - Coq
Mechanized formalization of Implicit resolution in Agda
-
Updated
Jun 28, 2017 - Agda
Learning formal proofs in mathematics/computer science/logic by formalizing them in the Agda language. A 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
Sep 13, 2020 - Agda
A Coq formalisation of the R programming language
-
Updated
Apr 28, 2020 - R
some sorting algorithms' formalisation
-
Updated
Aug 17, 2019 - Isabelle
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
An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.
-
Updated
Jul 31, 2018 - Common Lisp
Complexity analysis, type safety, soundness, etc.
-
Updated
May 8, 2020 - Agda
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.
-
Updated
Jul 23, 2020 - TeX
[alpha] An implementation of several classic transition systems that describe algorithms for SAT or SMT, for interactive exploration
-
Updated
Mar 10, 2020 - OCaml
Certified implementation of a parametrized framework for concurrent garbage collectors
-
Updated
Dec 4, 2016 - Coq
Solving the mini Rubik (2x2) in Coq
-
Updated
Aug 27, 2020 - Coq
A random collection of Agda facts around the Theory of Group Actions
-
Updated
Oct 18, 2020 - Agda
A proof of Stålmarck's algorithm in Coq [maintainer=@palmskog]
-
Updated
Sep 12, 2020 - Coq
-
Updated
Oct 22, 2020 - Coq
-
Updated
May 29, 2017 - HTML
Homeworks for 'formal languages and grammars' discipline
-
Updated
Apr 20, 2017 - C++
Improve this page
Add a description, image, and links to the formalization topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the formalization topic, visit your repo's landing page and select "manage topics."
++and--aren't required, but we should have them.https://pubs.opengroup.org/onlinepubs/9699919799/utilities/V3_chap02.html#tag_18_06_04