354 papers · page 1 of 18
We present an intrinsic representation of type theory in the proof assistant Cubical Agda, inspired by Awodey’s natural models of type theory. The initial natural model is defined as quotient inductive-inductive-recursive types, leading us to a syntax accepted by Cubical Agda wit…
Step-indexing and the later modality ▷ P are widely used in program logics. A key challenge in proofs in step-indexed logics is turning ▷ P into P, coined the later elimination problem. Later elimination cannot be done unconditionally, and has traditionally been linked one-to-one…
We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The s…
Verifying cache coherence protocols is a notoriously difficult problem. At the intersection between distributed protocol and computer architecture, it has long served as a premier target for formal methods. Current verification approaches hinge on the challenging discovery of lar…
The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the universal divided power algebra. This is an analogue, in the theory of divided powers, of the classical alg…
While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word p…
Data structures based on trees and tree traversals are ubiquitous in computer systems. Many low-level programs, including some implementations of critical systems like page tables and the web browser DOM, rely on generic tree-traversal functions that traverse tree nodes in a pre-…
The type system of Rust enforces the “shared xor mutable” principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of interior mutability. Thus, supporting interior mutability i…
We report on the higher-order differential calculus library developed inside the Lean mathematical library Mathlib. To support a broad range of applications, we depart in several ways from standard textbook definitions: we allow arbitrary fields of scalars, we work with functions…
Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs. We present logical pinning, a lightweight borrowing model …
This paper introduces slam, an Isabelle/HOL tactic and automated theorem prover based on the λ-superposition calculus. An alternative to Isabelle’s metis tactic, slam targets higher-order logic directly, avoiding the overhead introduced by metis’s translations to first-order logi…
This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard…
Finite Transducers (FTs) extend the capabilities of Finite Au- tomata (FAs) by enabling the transformation of input strings into output strings. In many practical applications — includ- ing program analysis, string constraint solving, and analysis of security-critical sanitizers …
Game trees are a fundamental mathematical abstraction for analyzing games, often implemented as rose trees in functional programming. We can construct rose trees by starting from an initial state and iteratively applying the function that provides the states one move away, an app…
In constructive commutative algebra, we revive the bar inductive characterization of Noetherian rings. We contribute the first constructive (axiom free) implementation of Hilbert's basis theorem, in the Rocq proof assistant. We show that the polynomial ring R[X] is Noetherian whe…
This paper describes Brack, which is a new verified compiler for Scheme. Brack compiles a substantial subset of Scheme, including first-class continuations, recursive bindings, first-class functions, mutable local variables, and lists, to CakeML, from where programs can be compil…
In modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by …
Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract treatment of the complex gluing models by internalizing the gluing category into a modal dependent t…
Probabilistic programs have a myriad of applications, from randomized algorithms to statistical modeling, and as such have inspired a long tradition of probabilistic program logics to verify their correctness. One essential use of probabilistic programs is to program new samplers…
Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions is necessary in many applications, such as formally verifying dynamic systems. Doing this automatically generally requires costly and intricate methods, which limits their …