isabelle-hol
There are 51 repositories under isabelle-hol topic.
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
au-ts/cogent
Cogent Project
jaalonso/Lecturas_GLC
Readings on computational logic, interactive theorem proving and functional programming.
jaalonso/Calculemus2
Proof exercises in Lean4 and Isabelle/HOL
marco10507/formalization-of-sorting-algorithms
some sorting algorithms' formalisation
diekmann/kant
Kategorischer Imperativ in Isabelle/HOL (experimental)
logicalhacking/Featherweight_OCL
Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
adbrucker/isabelle-hacks
A Collection of Isabelle Programming Hacks
diekmann/Isabelle-Hello-World
Hello World in Isabelle, compiled to Haskell
dominique-unruh/bounded-operators
Isabelle theory about bounded operators
jaalonso/RA20116
Curso de "Razonamiento automático"
Kuniwak/isabelle-program-semantics-exercise
「情報数学講座（第7巻）プログラム意味論」（著: 横内寛文）の形式的証明
lukaskollmer/advent-of-code
Advent of Code solutions, in OCaml and (sometimes) Isabelle/HOL
SvenWille/LogicForwardProofs
Propositional logic and FOL proofs (froward style)
appgvs/fv-project
Formally Verified Conflict-Free Replicated Data Types
ata-keskin/martingales
A Formalization of Martingales using Isabelle/HOL
aureleeNet/formalizations
This repository collects project-relevant Isabelle/HOL formalizations.
celinadongye/Geometry-of-Sections
Theorem proving geometry of sections in Isabelle
chrisdalvit/zeckendorf-theorem
A formal proof of the Zeckendorf theorem in Isabelle/HOL
cmadlener/isabelle-online-matching-primal-dual
Formal Primal-Dual Analysis of Online Matching Algorithms
Davetbutler/formalising-mpc-isabelle
Formalisation of MPC in Isabelle/HOL
go-pluto/verification
Verification-related documentation and code for pluto.
HaskDev0/Linear-Logic-Cat-semantics
Categorical Semantics of Intuitionistic Multiplicative Linear Logic written in Isabelle/HOL
jaalonso/SLP
Semánticas de lenguajes de programación formalizadas en Isabelle/HOL
logicalhacking/isabelle-ofmc
Isabelle/OFMC - Linking OFMC and Isabelle/HOL
pilif0/bigraph
Formalization of Robin Milner's bigraphs in Isabelle/HOL
s-nandi/automated-proofs
A small and simple set of automated proofs written in Isabelle
tobias-rothmann/KZG-Polynomial-Commitment-Scheme
Bachelor Thesis - Formalizing the KZG Polynomial Commitment Scheme in Isabelle/HOL.
vishallama/fds_ss20
Lecture course on verified Functional Data Structures
VTrelat/Hopcroft_verif
Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis
ata-keskin/eudoxus-reals
An unusual construction of the real numbers using Isabelle/HOL
rhjs94/schutz-minkowski-space
Formalisation in Isabelle/HOL of Schutz' axioms for Minkowski spacetime (and theorems of Chapter 3).
sorenmulli/draw-isabelle
Viz Isabelle ⟨l, a, r⟩ graphs