Topic: "formalization"
EgbertRijke/HoTT-Intro 📦
An introductory course to Homotopy Type Theory
Language: Agda - Size: 7.11 MB - Last synced at: 17 days ago - Pushed at: almost 5 years ago - Stars: 365 - Forks: 28
GeoCoq/GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
Language: Coq - Size: 7.66 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 197 - Forks: 27
mgree/smoosh
The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
Language: OCaml - Size: 3.66 MB - Last synced at: 27 days ago - Pushed at: about 2 years ago - Stars: 118 - Forks: 5
loganrjmurphy/LeanEuclid
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Language: Lean - Size: 3.57 MB - Last synced at: about 6 hours ago - Pushed at: about 7 hours ago - Stars: 98 - Forks: 8
TheoWinterhalter/formal-type-theory
Formalising Type Theory in a modular way for translations between type theories
Language: Coq - Size: 1.48 MB - Last synced at: about 16 hours ago - Pushed at: over 7 years ago - Stars: 94 - Forks: 4
Lysxia/system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Language: Coq - Size: 12.7 KB - Last synced at: 30 days ago - Pushed at: about 2 months ago - Stars: 34 - Forks: 2
gallais/agda-presburger
Deciding Presburger arithmetic in agda
Language: Agda - Size: 155 KB - Last synced at: about 1 month ago - Pushed at: about 2 years ago - Stars: 31 - Forks: 3
artagnon/bonak
🧊 An indexed construction of semi-simplicial and semi-cubical sets
Language: TeX - Size: 4.06 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 28 - Forks: 3
annenkov/two-level
Two-Level Type Theory
Language: Lean - Size: 151 KB - Last synced at: 12 days ago - Pushed at: over 5 years ago - Stars: 28 - Forks: 1
jonsterling/coq-guarded-computational-type-theory
Language: Coq - Size: 421 KB - Last synced at: 14 days ago - Pushed at: about 7 years ago - Stars: 21 - Forks: 1
uds-psl/autosubst2
Official repository of the Autosubst 2 project.
Language: Haskell - Size: 128 KB - Last synced at: 11 days ago - Pushed at: almost 2 years ago - Stars: 20 - Forks: 5
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.
Language: TeX - Size: 52.7 MB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 19 - Forks: 2
ivashkev/math-formalizations
Formalization of some elementary mathematical theories in Coq
Language: Coq - Size: 2.34 MB - Last synced at: 23 days ago - Pushed at: about 5 years ago - Stars: 14 - Forks: 0
superhaNds/cwfs
Formalization of Categories with Families
Language: Agda - Size: 1.45 MB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 13 - Forks: 0
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.
Language: Agda - Size: 1.24 MB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 12 - Forks: 0
felko/linear-algebra
Linear algebra formalization in Agda
Language: Agda - Size: 499 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 12 - Forks: 0
a2435191/lean-logic-formalization
Formalize "Logic Notes" by Lou van den Dries in Lean
Language: Lean - Size: 32.2 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 11 - Forks: 0
vltanh/lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Language: Lean - Size: 67.4 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 11 - Forks: 0
harp-project/Core-Erlang-Formalization
Language: Coq - Size: 3.37 MB - Last synced at: 7 days ago - Pushed at: 8 days ago - Stars: 10 - Forks: 1
miculan/telegram-mtproto2-verification
Formal Verification of Telegram's MTProto 2.0
Language: Shell - Size: 150 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 10 - Forks: 0
lean-dojo/LeanMillenniumPrizeProblems
Formalization of the Millennium Problems in Lean4.
Language: C - Size: 3.17 MB - Last synced at: 21 days ago - Pushed at: about 1 month ago - Stars: 9 - Forks: 0
siraben/coq-wigderson
Formalization of Wigderson's graph coloring algorithm in Coq
Language: Coq - Size: 988 KB - Last synced at: 27 days ago - Pushed at: over 1 year ago - Stars: 9 - Forks: 3
capital-G/xenakis-workgroup
Material created during the Iannis Xenakis workgroup
Language: Jupyter Notebook - Size: 24.4 MB - Last synced at: 16 days ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 2
tchajed/goedel-t
Formalization of termination of Gödel's System T
Language: Coq - Size: 70.3 KB - Last synced at: 24 days ago - Pushed at: almost 4 years ago - Stars: 9 - Forks: 0
Mbodin/CoqR
A Coq formalisation of the R programming language
Language: R - Size: 2.94 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 0
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.
Language: Agda - Size: 4.67 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 1
Lysxia/coq-mtl
Formalized laws for mtl
Language: Coq - Size: 56.6 KB - Last synced at: 27 days ago - Pushed at: over 5 years ago - Stars: 7 - Forks: 0
ajrouvoet/implicits.agda
Mechanized formalization of Implicit resolution in Agda
Language: Agda - Size: 510 KB - Last synced at: about 1 year ago - Pushed at: almost 8 years ago - Stars: 6 - Forks: 0
matematiflo/CompAssistedMath2024
GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.
Language: Jupyter Notebook - Size: 110 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 5 - Forks: 13
choukh/agda-veblen
veblen function in agda
Language: Agda - Size: 182 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0
marco10507/formalization-of-sorting-algorithms
some sorting algorithms' formalisation
Language: Isabelle - Size: 665 KB - Last synced at: about 1 year ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 0
Gradual-Typing/LambdaIFCStar
The Agda mechanization of a gradual security-typed programming language with general mutable references.
Language: Agda - Size: 971 KB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 4 - Forks: 1
thery/minirubik
Solving the mini Rubik (2x2) in Coq
Language: Coq - Size: 165 KB - Last synced at: 27 days ago - Pushed at: 5 months ago - Stars: 4 - Forks: 0
vitalsong/bastard
more than just a package manager
Language: CMake - Size: 55.7 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 4 - Forks: 1
snow0815/tribAIn
tribAin - ontology for scientific experiments in the domain of tribology
Size: 1.36 MB - Last synced at: 4 months ago - Pushed at: over 4 years ago - Stars: 4 - Forks: 3
jjaassoonn/flat 📦
Equivalent definitions of flatness
Language: Lean - Size: 813 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 3 - Forks: 0
UniFormal/VSCode-MMT
MMT plugin for Visual Studio Code
Language: TypeScript - Size: 442 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 3 - Forks: 0
jeffreybakker/wsn
Calculating the Risk of Valve Failures when Maintaining Water Supply Networks
Language: Python - Size: 105 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0
zchn/eth-acl2
An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.
Language: Common Lisp - Size: 249 KB - Last synced at: 6 months ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 3
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.
Language: TeX - Size: 877 KB - Last synced at: 29 days ago - Pushed at: almost 5 years ago - Stars: 3 - Forks: 0
choukh/agda-googology
formalized googology in agda
Language: CSS - Size: 3.75 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 2 - Forks: 0
co-dan/BI-cutelim
Cut elimination for the logic of Bunched Implications (BI), and some extensions.
Language: Coq - Size: 769 KB - Last synced at: 10 days ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 1
siraben/senior-thesis
LaTeX sources for my undergraduate thesis
Language: TeX - Size: 791 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 1
sacerdot/Crumbling-Abstract-Machines
This repository contains the formalization of part of the theory behind the Crumbling Abstract Machines, that has been introduced and partially developed in Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY,USA,39 pages.
Language: Mathematica - Size: 854 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 1
lukaszcz/sortalgs
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Language: Coq - Size: 23.4 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0
zampino/ggt
A random collection of Agda facts around the Theory of Group Actions
Language: Agda - Size: 40 KB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 2 - Forks: 0
benhuds/Agda
Complexity analysis, type safety, soundness, etc.
Language: Agda - Size: 1.21 MB - Last synced at: about 2 months ago - Pushed at: almost 5 years ago - Stars: 2 - Forks: 0
kiranandcode/CamelClone
Automatically push changes to selected repositories - 0% tested yet 100% correct.
Language: Coq - Size: 13.7 KB - Last synced at: 12 days ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 0
cogumbreiro/habanero-coq
Coq formalization of the Habanero programming model.
Language: Coq - Size: 1020 KB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0
thery/Selinger
Formalisation of Selinger proof about quantum gate
Language: Coq - Size: 208 KB - Last synced at: 12 days ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0
thery/EdwardsEllipticCurve
Group Law for Elliptic Curves according to Tom Hales
Language: Coq - Size: 277 KB - Last synced at: 12 days ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0
metinersin/FormalTextbookModelTheory
Language: HTML - Size: 869 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0
themathqueen/monlib4
Formalising non-commutative graph theory in Lean
Language: Lean - Size: 917 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0
pitmonticone/FLT3 Fork of riccardobrasca/flt3
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Language: TeX - Size: 550 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 1
bakseter/thesis
My master thesis (and related code) in Logic at the University of Bergen.
Language: Haskell - Size: 7.48 MB - Last synced at: 20 days ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0
ata-keskin/martingales
A Formalization of Martingales using Isabelle/HOL
Language: Isabelle - Size: 20 MB - Last synced at: 21 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
choukh/MetaLogic
first-order logic and set theory
Language: Agda - Size: 340 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
jjaassoonn/twist
Definition of Serre's twisting sheaf (work in progress)
Language: Lean - Size: 62.5 KB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 1
jjaassoonn/cc
Čech cohomology on topological space
Language: Lean - Size: 229 KB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0
imandra-ai/abstract-transition-systems
[alpha] An implementation of several classic transition systems that describe algorithms for SAT or SMT, for interactive exploration
Language: OCaml - Size: 229 KB - Last synced at: 3 days ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 1
radeusgd/pDOT-GADT
Formal foundations for GADTs in Scala
Language: Scala - Size: 519 KB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
fasapa/lambdaex
Specification, formalization and verification of the XC function from ex lambda calculus in Coq.
Language: Coq - Size: 135 KB - Last synced at: 9 months ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0
pilif0/bigraph
Formalization of Robin Milner's bigraphs in Isabelle/HOL
Language: Isabelle - Size: 12.7 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0
nickgian/Bonsai-coq
A formalization of SRPs and Control Plane Compression in Coq.
Language: Coq - Size: 6.84 KB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0
UCL-PPLV/GCTransformations
Certified implementation of a parametrized framework for concurrent garbage collectors
Language: Coq - Size: 248 KB - Last synced at: 9 months ago - Pushed at: over 8 years ago - Stars: 1 - Forks: 1
Danelnov/Lambda-Calculus-Formalization-
This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem
Language: Lean - Size: 2.93 KB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 0 - Forks: 0
FMFI-UK-1-AIN-412/formalization-checker-backend
The back end of a tool for checking formalization exercises.
Language: JavaScript - Size: 247 KB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 5
UFrameIT/archives
All MMT archives of formalizations needed by the UFrameIT prototype in the FrameIT project.
Language: Shell - Size: 62.5 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0
krr-up/flatland-formalization-notes
A space for the formalization of the underlying structure of Flatland.
Language: TeX - Size: 2.5 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
ewdlop/FormalML Fork of IBM/FormalML
Formalization of Machine Learning Theory with Applications to Program Synthesis
Language: Coq - Size: 8.84 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
FormalMathematicsLab/ICL_Course_FormalMathematics_2024 Fork of ImperialCollegeLondon/formalising-mathematics-2024
Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).
Language: Lean - Size: 356 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 0 - Forks: 0
SDZZGNDRC/LADR
Formalizing "Linear Algebra Done Right" using Lean
Language: Lean - Size: 39.1 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0
pitmonticone/carleson Fork of fpvandoorn/carleson
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
Language: TeX - Size: 1.31 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
Seeker04/stlc-agda-elab
Agda formalisation of an elaborator for a simply typed language
Language: Agda - Size: 4.98 MB - Last synced at: 2 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
FormalMathematicsLab/LFTCM2024 Fork of riccardobrasca/LFTCM2024
Repository hosting resources for the 2024 workshop "Lean for the Curious Mathematician".
Language: Lean - Size: 693 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
FormalMathematicsLab/UniRome_Workshop_Lean_2024 Fork of fpvandoorn/LeanInRome
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
Size: 2.6 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
ata-keskin/eudoxus-reals
An unusual construction of the real numbers using Isabelle/HOL
Language: Isabelle - Size: 814 KB - Last synced at: 4 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
miguelpagano/formalmetatheory-stoughton Fork of ernius/formalmetatheory-stoughton
We prove the equivalence between three induction principles for the untyped lambda calculus.
Language: Agda - Size: 2.97 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
haztecaso/euclidean-geometry-lean
Trabajo de Fin de Grado de Matemáticas, en la Universidad Complutense de Madrid. Presentado en septiembre de 2023.
Language: TeX - Size: 40.4 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
bridgekat/leansubst
An Autosubst-like tool for handling de Bruijn indices / 一个和 Autosubst 类似的用于处理 de Bruijn 标号的工具
Language: Lean - Size: 54.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
FMFI-UK-1-AIN-412/formalization-checker
The front end of a tool for checking formalization exercises.
Language: JavaScript - Size: 5.91 MB - Last synced at: 23 days ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 5
dfirsov/easycrypt-zk-code
EasyCrypt formalization of definitions and derivations associated with zero-knowledge (sigma protocols).
Language: eC - Size: 759 KB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
MathiasGarnier/formalean-inator
Aiming to have a personal well-founded math library written in lean. Hope it works...
Size: 62.5 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
Paul-Lez/dedekind-kummer-theorem
This repository will eventually contain the code I wrote when formalising the Dedekind-Kummer Theorem
Size: 2.93 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
Kamirus/fine-grained-shift0-dollar
Coq Formalisation of "A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar"
Language: Coq - Size: 532 KB - Last synced at: 20 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
BlueHuskyStudios/Blue-Husky-Stages-of-Product-Creation
The stages that Blue Husky Studios goes throguh when creating a product
Size: 7.81 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
pedroos/limits
Mathematical foundations exploration
Language: C# - Size: 268 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0
danielneubert/Reform.js 📦
Modern forms finally made easy.
Language: JavaScript - Size: 225 KB - Last synced at: 15 days ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0
enshankar/BigProof
Collaborative repo for Big Proof Programme at the Isaac Newton Institute, Jun 26 to Aug 4, 2017
Size: 20.5 KB - Last synced at: over 1 year ago - Pushed at: almost 8 years ago - Stars: 0 - Forks: 0
ankitku/Twisted_Functor_Verification
Language: HTML - Size: 22.5 KB - Last synced at: about 2 years ago - Pushed at: almost 8 years ago - Stars: 0 - Forks: 0
ahovgaard/twelf-records
Formalization of a simple functional language with records and subtyping in Twelf.
Size: 12.7 KB - Last synced at: about 2 years ago - Pushed at: about 8 years ago - Stars: 0 - Forks: 0
zeionara/formal_languages_and_grammars
Homeworks for 'formal languages and grammars' discipline
Language: C++ - Size: 419 KB - Last synced at: 2 months ago - Pushed at: about 8 years ago - Stars: 0 - Forks: 0
