Search
Search Results
-
Linear Resources in Isabelle/HOL
We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of...
-
Mechanising Gödel–Löb Provability Logic in HOL Light
We introduce our implementation in HOL Light of the metatheory for Gödel–Löb provability logic (GL), covering soundness and completeness w.r.t....
-
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search...
-
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL
We present a formalization of several fundamental notions and results from Quantum Information theory in the proof assistant Isabelle/HOL, including...
-
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and...
-
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
Special relativity is a cornerstone of modern physical theory. While a standard coordinate model is well known and widely taught today, multiple...
-
ULKB Logic: A HOL-Based Framework for Reasoning over Knowledge Graphs
ULKB Logic is an open-source framework written in Python for reasoning over knowledge graphs. It provides an interactive theorem prover-like... -
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore,... -
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL
Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style...
-
Verifying Feedforward Neural Networks for Classification in Isabelle/HOL
Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural... -
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a... -
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal... -
Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem
Free groups are central to group theory, and are ubiquitous across many branches of mathematics, including algebra, topology and geometry. An... -
Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL
The verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions,... -
A Verified Implementation of B \(^+\) -Trees in Isabelle/HOL
In this paper we present the verification of an imperative implementation of the ubiquitous B... -
Certified Quantum Computation in Isabelle/HOL
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant...
-
Lyndon Words Formalized in Isabelle/HOL
We present a formalization of Lyndon words and basic relevant results in Isabelle/HOL. We give a short review of Isabelle/HOL and focus on challenges... -
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To... -
Verifying Secure Speculation in Isabelle/HOL
Secure speculation is an information flow security hyperproperty that prevents transient execution attacks such as Spectre, Meltdown and Foreshadow....