Related papers: Constructive Galois Connections: Taming the Galois…
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections using proof assistants remains limited to…
Calculational abstract interpretation, long advocated by Cousot, is a technique for deriving correct-by-construction abstract interpreters from the formal semantics of programming languages. This paper addresses the problem of deriving…
Abstract interpretation-based static analyses rely on abstract domains of program properties, such as intervals or congruences for integer variables. Galois connections (GCs) between posets provide the most widespread and useful formal tool…
The design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work to implement an analyzer and prove it sound. In short, static…
We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior…
It is argued that a broad class of AGI-relevant algorithms can be expressed in a common formal framework, via specifying Galois connections linking search and optimization processes on directed metagraphs whose edge targets are labeled with…
We offer a lattice-theoretic account of dynamic slicing for {\pi}-calculus, building on prior work in the sequential setting. For any run of a concurrent program, we exhibit a Galois connection relating forward slices of the start…
A Galois connection between clones and relational clones on a fixed finite domain is one of the cornerstones of the so-called algebraic approach to the computational complexity of non-uniform Constraint Satisfaction Problems (CSPs). Cohen…
Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing program behavior. In recent work, Yao et al. scaled semantic…
Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees.…
We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions - a topic known as higher-order abstract interpretation. We are motivated by the…
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically…
The Galois lattice is a graphic method of representing knowledge structures. The first basic purpose in this paper is to introduce a new class of Galois lattices, called graded Galois lattices. As a direct result, one can obtain the notion…
We prove a Galois-type correspondence between compositions of purely inseparable field extensions (including infinite ones) and subalgebras of differential operators. This correspondence can be utilized to establish a connection between…
Causal abstraction provides a theoretical foundation for mechanistic interpretability, the field concerned with providing intelligible algorithms that are faithful simplifications of the known, but opaque low-level details of black box AI…
In this preprint we present an outline of the multidimensional version of topological Galois theory. The theory studies topological obstruction to solvability of equations "in finite terms" (i.e. to their solvability by radicals, by…
Labelling-based formal argumentation relies on labelling functions that typically assign one of 3 labels to indicate either acceptance, rejection, or else undecided-to-be-either, to each argument. While a classical labelling-based approach…
An algebraic technique is presented that does not use results of model theory and makes it possible to construct a general Galois theory of arbitrary nonlinear systems of partial differential equations. The algebraic technique is based on…
In the preprint we present an outline of the one dimensional version of topological Galois theory. The theory studies topological obstruction to solvability of equations "in finite terms" (i.e. to their solvabilty by radicals, by elementary…
These notes are an exposition of Galois Theory from the original Lagrangian and Galoisian point of view. A particular effort was made here to better understand the connection between Lagrange's purely combinatorial approach and Galois…