Front Matter, Table of Contents, Preface, Conference Organization
Front Matter, Table of Contents, Preface, Conference Organization
26,098 papers · page 45 of 1,305
Mono Types - First-Class Containers for Datalog
We propose mono types, a new abstraction for programming Datalog. Mono types behave like first-class containers that can be stored in relations and to which elements can be added decentrally. But, mono types are more than just containers: They provide a read operation that can yi…
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interp…
Chain of Grounded Objectives: Concise Goal-Oriented Prompting for Code Generation
The use of Large Language Models (LLMs) for code generation has gained significant attention in recent years. Existing methods often aim to improve the quality of generated code by incorporating additional contextual information or guidance into input prompts. Many of these appro…
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch-and-bound (BaB) is a "divide-and-conquer" strategy that applies off-the-sh…
The Vanilla Sequent Calculus is Call-by-Value
Abstract Existing Curry-Howard interpretations of call-by-value evaluation for the $$\lambda $$ λ -calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact th…
Formulas as Processes, Deadlock-Freedom as Choreographies
Abstract We introduce a novel approach to studying properties of processes in the $$\pi $$ π -calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics …
Sufficient Conditions for Robustness of RDMA Programs
Abstract Remote Direct Memory Access (RDMA) is a modern technology enabling high-performance inter-node communication. Despite its widespread adoption, theoretical understanding of permissible behaviours remains limited, as RDMA follows a very weak memory model. This paper addres…
Constructive characterisations of the MUST-preorder for asynchrony
Abstract De Nicola and Hennessy’s $$\textsc {must}$$ M U S T -preorder is a liveness preserving refinement which states that a server $$q$$ q refines a server $$p$$ p if all clients satisfied by $$p$$ p are also satisfied by $$q$$ q . Owing to the universal quantification over cl…
Abstraction of memory block manipulations by symbolic loop folding
Abstract We introduce a new abstract domain for analyzing memory block manipulations, focusing on programs with dynamically allocated arrays. This domain computes properties universally quantified over the value of the loop counters, both for assignments and tests. These properti…
Cognacy Queries over Dependence Graphs for Transparent Visualisations
Abstract Charts, figures, and text derived from data play an important role in decision making. But making sense of or fact-checking outputs means understanding how they relate to the underlying data. Even for experts with access to the source code and data sets, this poses a sig…
An abstract, certified account of operational game semantics
Abstract Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given p…
Artifact Report: an Abstract, Certified Account of Operational Game Semantics
Abstract This artifact report is a companion to the ESOP’25 paper An abstract, certified account of operational game semantics [3]. The paper describes the construction of a sound model for an abstract notion of language. The model is built using a semantic technique named Operat…
Multiparty Session Types with a Bang!
Abstract Replication is an alternative construct to recursion for describing infinite behaviours in the $$\pi $$ π -calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-pa…
Stratified Type Theory
Abstract A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type axiom. In this work, we argue that a universe hierarchy is not t…
Neural Network Verification is a Programming Language Challenge
Abstract Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or uni…
Variable Elimination as Rewriting in a Linear Lambda Calculus
Abstract Variable Elimination ( $$\textsf{VE}$$ VE ) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Eli…
Coverage Semantics for Dependent Pattern Matching
Abstract Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating …
A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model
Abstract Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic supporting thread-l…
Iso-Recursive Multiparty Sessions and their Automated Verification
Abstract "Image missing""Image missing" Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised mul…