Related papers: General Bindings and Alpha-Equivalence in Nominal …
Using Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then,…
We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $\beta\eta$-equivalence classes of…
This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of signature for specifying objects of a given category as initial objects in a suitable…
Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL…
The notion of $\alpha$-equivalence between $\lambda$-terms is commonly used to identify terms that are considered equal. However, due to the primitive treatment of free variables, this notion falls short when comparing subterms occurring…
In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching…
Formal theorem proving, a field at the intersection of mathematics and computer science, has seen renewed interest with advancements in large language models (LLMs). This paper introduces SubgoalXL, a novel approach that synergizes…
We propound the thesis that there is a limitation to the number of possible structures which are axiomatically endowed with identities involving operations. In the case of algebras with a binary operation satisfying a formally reducible (to…
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave)…
Functional analysis, especially the theory of Hilbert spaces and of operators on these, form an important area in mathematics. We formalized the Isabelle/HOL library Complex_Bounded_Operators containing a large amount of theorems about…
Let $A_{1},...A_{m}$ be a $n\times n$ invertible matrices. Let $0 \leq \alpha<n$ and $0<\alpha_{i}<n$ such that $\alpha_1 + ... + \alpha_m = n- \alpha$. We define% \begin{equation*} T_{\alpha}f(x)=\int \frac{1}{\left\vert…
The bounded derived category of a finite dimensional algebra of finite global dimension is equivalent the stable category of $\mathbb{Z}$-graded modules over its trivial extension \cite{Happel}. In particular, given two derived equivalent…
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using…
In this note, we provide bijective proofs of some identities involving the Bell number, as previously requested. Our arguments may be extended to yield a generalization in terms of complete Bell polynomials. We also provide a further…
A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computation results of free-roaming mobile agents doing comparison…
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial…
This paper provides a new categorification of the Lebesgue integral with variable upper limits by using normed modules over finite-dimensional $\Bbbk$-algebras $\mathit{\Lambda}$ and the category $\mathscr{A}^p_{\mathit{\Lambda}}$…
Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and…
We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade…
We prove a general congruence result for bisimilarity in higher-order languages, which generalises previous work to languages specified by a labelled transition system in which programs may occur as labels, and which may rely on operations…