Topic: "coq-formalization"
MetaRocq/metarocq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Language: Coq - Size: 33.8 MB - Last synced at: 7 days ago - Pushed at: 10 days ago - Stars: 437 - Forks: 88
verse-lab/ceramist
Verified hash-based AMQ structures in Coq
Language: Coq - Size: 1.04 MB - Last synced at: 6 months ago - Pushed at: about 5 years ago - Stars: 122 - Forks: 5
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
Language: Coq - Size: 596 KB - Last synced at: 18 days ago - Pushed at: 6 months ago - Stars: 95 - Forks: 4
bluerock-io/BRiCk
Formalization of C++ for verification purposes.
Language: Coq - Size: 89.8 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 80 - Forks: 14
INRIA/velus
A Lustre compiler in Coq
Language: Coq - Size: 9.76 MB - Last synced at: 16 days ago - Pushed at: 21 days ago - Stars: 66 - Forks: 6
SSProve/ssprove
A foundational framework for modular cryptographic proofs in Coq
Language: Coq - Size: 3.28 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 64 - Forks: 13
sigurdschneider/lvc
LVC verified compiler
Language: Coq - Size: 5.64 MB - Last synced at: 18 days ago - Pushed at: over 6 years ago - Stars: 57 - Forks: 2
Blaisorblade/dot-iris
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
Language: HTML - Size: 9.98 MB - Last synced at: 11 days ago - Pushed at: about 1 month ago - Stars: 31 - Forks: 1
llee454/functional-algebra
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
Language: Coq - Size: 1.95 MB - Last synced at: 9 months ago - Pushed at: about 6 years ago - Stars: 28 - Forks: 2
verif-scop/PolCert
A verified polyhedral scheduling validator in Coq.
Language: Coq - Size: 2.1 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 17 - Forks: 1
VERIMAG-Polyhedra/VPL
Verimag Polyhedra Library
Language: OCaml - Size: 1.4 MB - Last synced at: 11 months ago - Pushed at: almost 5 years ago - Stars: 17 - Forks: 2
yiyunliu/mltt-consistency
Logical relation for predicative CC omega with booleans and an intensional identity type
Language: TeX - Size: 7.93 MB - Last synced at: 6 days ago - Pushed at: about 2 months ago - Stars: 12 - Forks: 2
thery/grobner
A fornalisation of Grobner basis in ssreflect
Language: Coq - Size: 90.8 KB - Last synced at: 21 days ago - Pushed at: 4 months ago - Stars: 12 - Forks: 3
uds-psl/CoqTM
Formalising Turing Machines In Coq (bachelor's thesis)
Language: Coq - Size: 1.32 MB - Last synced at: 2 days ago - Pushed at: almost 2 years ago - Stars: 12 - Forks: 2
acorrenson/automatik
A library of formalized automaton algorithms
Language: Coq - Size: 25.4 KB - Last synced at: 20 days ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 1
PnVDiscord/PnVRocqLib
A Coq library written by members of PnV Discord Server
Language: Coq - Size: 349 KB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 8 - Forks: 1
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
thery/lemonde
les problèmes proposés par le journal Le Monde en Coq
Language: Coq - Size: 97.7 KB - Last synced at: 18 days ago - Pushed at: 4 months ago - Stars: 7 - Forks: 0
bor0/formal-ed
Paper: Formalizing line editors in Coq
Language: TeX - Size: 12.7 KB - Last synced at: 14 days ago - Pushed at: almost 5 years ago - Stars: 7 - Forks: 0
thery/Plouffe
Computing Pi decimal using Plouffe Formula in Coq
Language: Coq - Size: 56.6 KB - Last synced at: 18 days ago - Pushed at: 4 months ago - Stars: 6 - Forks: 1
TheoWinterhalter/ett-to-wtt
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
Language: Coq - Size: 630 KB - Last synced at: 25 days ago - Pushed at: almost 2 years ago - Stars: 6 - Forks: 0
thery/FlocqLecture
Language: Coq - Size: 30.3 KB - Last synced at: 18 days ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 1
lukaszcz/COQ-IMP
Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.
Language: Coq - Size: 68.4 KB - Last synced at: 2 days ago - Pushed at: about 3 years ago - Stars: 6 - Forks: 1
jgrosso/coq-alpha-pearl
Coq formalization of "Functional Pearls: α-conversion is easy" (Altenkirch, 2002).
Language: Coq - Size: 1.01 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 5 - Forks: 0
thery/twoSquare
A proof of Fermat's theorem on sum of two squares with mathcom using gaussian integers.
Language: Coq - Size: 135 KB - Last synced at: 17 days ago - Pushed at: 4 months ago - Stars: 4 - Forks: 1
Kamirus/lambda-formalizations
Lambda Calculi Formalizations in Coq using nested datatypes for a type-safe term representation
Language: Coq - Size: 388 KB - Last synced at: 22 days ago - Pushed at: over 2 years ago - Stars: 4 - Forks: 1
DmxLarchey/Coq-is-total
A proof that Coq contains any total mu-recursive function
Language: Coq - Size: 87.9 KB - Last synced at: 3 days ago - Pushed at: about 7 years ago - Stars: 4 - Forks: 0
plietar/formal-pony
Language: Coq - Size: 43.9 KB - Last synced at: 21 days ago - Pushed at: about 8 years ago - Stars: 4 - Forks: 0
thery/robbins
Proof in Coq that all Robbins algebras are Boolean algebras
Language: Coq - Size: 33.2 KB - Last synced at: 17 days ago - Pushed at: 4 months ago - Stars: 3 - Forks: 1
thery/GeometricAlgebra Fork of olivierverdier/GeometricAlgebra
Work based on http://www-sop.inria.fr/marelle/GeometricAlgebra/
Language: Coq - Size: 281 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 3
jinxinglim/coq-formalized-divide-and-conquer
This respository contains the formalization of different variations of divide-and-conquer algorithm design paradigm for lists. As a case study, we will see how these different variations lead to different sorting algorithms.
Language: Coq - Size: 42 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0
wkolowski/CoqCat
Formalization of Category Theory in Coq.
Language: Coq - Size: 1.24 MB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 2
thery/sudoku 📦
Sudoku in Coq
Language: Coq - Size: 137 KB - Last synced at: about 2 months ago - Pushed at: over 3 years ago - Stars: 3 - Forks: 0
kaist-cp/view-hw
Mechanized Proof for Article: "Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8" (PLDI 2021)
Language: Coq - Size: 1.41 MB - Last synced at: 16 days ago - Pushed at: about 4 years ago - Stars: 3 - Forks: 0
rudynicolop/TAPL-Coq
Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages
Language: Coq - Size: 494 KB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 1
tilk/LambdaCert Fork of progval/LambdaCert
Certified LambdaJS semantics and interpreter.
Language: Coq - Size: 4.5 MB - Last synced at: 12 months ago - Pushed at: about 8 years ago - Stars: 3 - Forks: 0
ComFreek/basic-ontology-language
An experimental ontology language formalized in Coq with many semantics
Language: Coq - Size: 816 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0
valoran-M/diqt
Formalization of hashtables with Radix trees and PArray in Coq
Language: Coq - Size: 2.19 MB - Last synced at: 6 days ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0
lukaszcz/sortalgs
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Language: Coq - Size: 23.4 KB - Last synced at: about 2 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0
TypicalMath/subst-interpol
Uniform Interpolation for some Substructural Logics (work in progress)
Language: Coq - Size: 19.5 KB - Last synced at: about 1 month ago - Pushed at: about 5 years ago - Stars: 2 - Forks: 0
ak-fr/voronoi-fortune
Fortune's algorithm described in coq
Language: Coq - Size: 4.85 MB - Last synced at: about 1 month ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 1
boulme/satans-cert
Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)
Language: Coq - Size: 30.4 MB - Last synced at: almost 2 years ago - Pushed at: about 6 years ago - Stars: 2 - Forks: 0
llee454/pigeons
A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.
Language: Makefile - Size: 39.1 KB - Last synced at: about 2 months ago - Pushed at: about 6 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
TheoWinterhalter/local-comp
WIP Local computation rules in type theory
Language: Coq - Size: 215 KB - Last synced at: 8 days ago - Pushed at: 9 days ago - Stars: 1 - Forks: 0
dcastrop/coq-hylomorphisms
(Terminating) hylomorphisms in Coq
Language: Coq - Size: 833 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 0
dot-iris/dot-iris.github.io
GitHub Pages website for https://github.com/Blaisorblade/dot-iris.
Language: HTML - Size: 10.4 MB - Last synced at: 2 months ago - Pushed at: 2 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: 3 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0
branebb/simply-typed-lambda-calculus
Final project for master's degree in Semantics of programming languages course.
Language: Haskell - Size: 8.79 KB - Last synced at: 11 days ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0
yiyunliu/takahashi-factorization
A proof of factorization using Takahashi's method
Language: Coq - Size: 21.5 KB - Last synced at: 14 days ago - Pushed at: 10 months ago - Stars: 1 - Forks: 1
DenSinH/natural-numbers-game
A version of the natural numbers game in Coq
Language: Coq - Size: 402 KB - Last synced at: 11 days ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0
thery/huffman Fork of coq-community/huffman
A correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
Language: Coq - Size: 188 KB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0
hivert/Coq-Combi Fork of math-comp/Coq-Combi
Algebraic Combinatorics in Coq
Size: 9.92 MB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0
rikosellic/ZFC-prover-in-Coq
A mini ZFC prover embedded in Coq for teaching scenarios. (CoqPL'23)
Language: Coq - Size: 107 KB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 1
klausnat/Adam_Chlipala_Certified_Programming_with_Dependent_Types_Exercises
COQ. Certified Programming with Dependent Types by Adam Chlipala. Exercises from the book. Solutions.
Language: Coq - Size: 27.3 KB - Last synced at: 10 days ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0
erwanM974/coq_hibou_label_multi_trace_analysis
Formal proof with the Coq theorem prover of the correctness of an oracle algorithm for offline analysis of distributed logs against interaction models
Language: HTML - Size: 105 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0
erwanM974/coq_hibou_label_equivalent_terms
Formal proof with the Coq theorem prover that elements of some equivalence classes defined over a formal language of interactions describing the behavior of distributed systems have the same semantics.
Language: HTML - Size: 46.9 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 1 - Forks: 1
spidermoy/LTL_Coq
Linear Temporal Logic formalized in Coq
Language: Coq - Size: 28.3 KB - Last synced at: 7 months ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 2
spidermoy/Monads_KleisliTriples_Proof
Computer Scientist Degree - Thesis Work
Language: Coq - Size: 573 KB - Last synced at: 7 months ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
cs-t1/PyMaths
Modélisation de concepts mathématiques et raisonnements sur ces derniers.
Language: Python - Size: 5.86 KB - Last synced at: 3 months ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
RSilviu/coq2sol
Formal semantics for Solidity in Coq
Language: Coq - Size: 73.2 KB - Last synced at: 7 months ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0
DmxLarchey/The-Tortoise-and-the-Hare
The Tortoise and the Hare in Coq. Constructive extraction via Bar inductive predicates (see README.md below).
Language: Coq - Size: 46.9 KB - Last synced at: 3 days ago - Pushed at: almost 7 years ago - Stars: 1 - Forks: 1
AnthonyBordg/UniLab
Formalized Mathematics
Language: Coq - Size: 76.2 KB - Last synced at: 10 days ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0
SkySkimmer/metacoq Fork of MetaRocq/metarocq
Metaprogramming in Coq
Language: Coq - Size: 28.1 MB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 0 - Forks: 0
aaditya29/Formal-Method-Proofs-by-Coq
Proofs in Coq
Language: Coq - Size: 45.9 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0
KiJeong-Lim/Fol-archived 📦
A New Coq Formalisation of Classical First-Order Logic with Proofs of the Soundness and Completeness Theorems
Language: Coq - Size: 884 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
motrellin/comoalg
Some personal notes on typical algebra topics
Language: Coq - Size: 87.9 KB - Last synced at: 11 days ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0
marek-bauer/Quotientlike-types-in-Coq
This is a repo of my master's thesis written as part of my studies at the University of Wrocław
Language: Coq - Size: 4.96 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
rikosellic/ExplicitLAM
Coq formalization of lambda calculus theories with explicit names. (SETTA'23)
Language: Coq - Size: 85 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
luizaugustogarcia/euclidean-algorithm
Demonstration, in Coq, that the Euclidean Algorithm can be efficiently used to compute the greatest common divisor of two numbers
Language: Makefile - Size: 19.5 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
roglo/coq_euler_prod_form
Coq proof of the Euler product formula for the Riemann zeta function (in progress...)
Language: Coq - Size: 1.52 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 1
DmxLarchey/Relevant-decidability
A constructive account of Kripke-Curry's decidability proof for Implicational Relevance logic (see README.md below)
Language: Coq - Size: 179 KB - Last synced at: 3 days ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 1
BelegCuthalion/stl
∇⎕ coloring
Language: TeX - Size: 249 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
jdmota/Harpers-E-Language-in-Coq
Harper's E Language in Coq
Language: Coq - Size: 465 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0
Chesium/GeoCoq-zh Fork of GeoCoq/GeoCoq
GeoCoq, Chinese translation.
Language: Coq - Size: 9.99 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
rudynicolop/Type-Reconstruction
Descriptions & implementations of type-reconstruction/inference algorithms.
Language: Coq - Size: 357 KB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
erwanM974/coq_hibou_label_semantics_equivalence
Formal proof with the Coq theorem prover of the equivalence of three semantics for a language describing the behavior of distributed systems.
Language: HTML - Size: 178 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0
ivanbakel/coq-SPAM
Formalisation of Separation Logic and Mutability
Language: Coq - Size: 20.5 KB - Last synced at: about 1 year ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0
rigille/continhas
Coq formalization of soroban algorithms
Language: Coq - Size: 4.88 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0
Champitoad/LambdaSub
Formalization in Coq of a simply typed λ-calculus extended with records and subtyping.
Language: Makefile - Size: 65.4 KB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
ajayeeralla/real-or-random-auth-proofs-coq
Machine-checked proofs of secrecy and authentication using CCSA framework
Language: Coq - Size: 2.37 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
Champitoad/CoqHopf
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
Language: HTML - Size: 402 KB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
anhmiuhv/fx10-coq
Language: Makefile - Size: 19.5 KB - Last synced at: 21 days ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0
ryuta-ito/algebra_1
practice
Language: Coq - Size: 43 KB - Last synced at: 6 months ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0
Champitoad/cbpv
A study of a simplified Call-By-Push-Value lambda-calculus in Coq.
Language: Coq - Size: 479 KB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 0 - Forks: 0
DabrowskiFr/Vector
A vector library specialized in the formalization of SPMD programs
Language: Coq - Size: 21.5 KB - Last synced at: over 1 year ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0
cogumbreiro/gorn-coq
Deadlock avoidance on using futures in shared memory. The project includes the formalization of a trace language and results on a policy on safe joins (through a notion of known tasks) and we show that data-race-freedom implies deadlock freedom.
Language: Coq - Size: 421 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 2
markisus/sum-one-to-n
Proof that the sum one to n is n*(n+1)/2 in Coq
Language: Coq - Size: 1000 Bytes - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0
chrisswhitneyy/CS499_MechanicalReasoning
Coq implementations and proof scripts developed for a course in mechanical reasoning.
Language: Coq - Size: 448 KB - Last synced at: about 2 years ago - Pushed at: almost 8 years ago - Stars: 0 - Forks: 0
