Schrödinger's hats: a puzzle about parities and permutations
-
Updated
May 10, 2017 - Isabelle
Schrödinger's hats: a puzzle about parities and permutations
Lecture course on verified Functional Data Structures
Theorem proving in Isabelle
Coursework for Automated Reasoning 2021/22 at the University of Edinburgh
A formalisation of Solèr's theorem using the Isabelle proof assistant
Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis
An automated equivalence reasoner for Isabelle/HOL
Bachelor Thesis - Formalizing the KZG Polynomial Commitment Scheme in Isabelle/HOL.
Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"
Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."