相关论文: Set Theory for Verification: I. From Foundations t…

A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts…

This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential…

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…

Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discourse contains only sets, and hence every mathematical object…

Modern functional-logic programming languages like Toy or Curry feature non-strict non-deterministic functions that behave under call-time choice semantics. A standard formulation for this semantics is the CRWL logic, that specifies a proof…

We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…

An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies…

This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization…

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning…

The standard axioms of set theory, the Zermelo-Fraenkel axioms (ZFC), do not suffice to answer all questions in mathematics. While this follows abstractly from Kurt G\"odel's famous incompleteness theorems, we nowadays know numerous…

Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search,…

We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems…

Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and…

In this paper, we propose the use of interactive theorem proving for explainable machine learning. After presenting our proposition, we illustrate it on the dedicated application of explaining security attacks using the Isabelle…

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the…

Consensus protocols are crucial for a blockchain system as they are what allow agreement between the system's nodes in a potentially adversarial environment. For this reason, it is paramount to ensure their correct design and implementation…

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 extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…

Choice and independence of premise principles play an important role in characterizing Kreisel's modified realizability and G\"odel's Dialectica interpretation. In this paper we show that a great many intuitionistic set theories are closed…