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
Coursework for Automated Reasoning 2021/22 at the University of Edinburgh
Theorem proving in Isabelle
Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.
Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"
Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis
A formalisation of Solèr's theorem using the Isabelle proof assistant
Lecture course on verified Functional Data Structures
Bachelor Thesis - Formalizing the KZG Polynomial Commitment Scheme in Isabelle/HOL.
An automated equivalence reasoner for Isabelle/HOL
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."