This work develops higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers.
Abstract
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.
Formally reasoning about Rust programs requires a rigorous formal semantics, especially in the context of deductive verification and concurrent programming. We present a modular, flexible semantics for a significant subset of (close to) source code level Rust, based on the recent locally abstract, globally concrete sem...
This paper establishes a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics, and covers a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabili...
Property-based testing of C programs can be automated by synthesizing random input generators from separation-logic specifications. Existing work in this space, such as the Bennet testing tool, uses randomized backtracking search, generating random values and checking them against constraints, backtracking on failure....
Zain K. Aamer, Benjamin C. Pierce· Proceedings of the ACM on Pr...· 1 citation
We propose endogenous interpretation: program, interpreter, machine, and derived execution language are not disjoint semantic objects but different parameterizations of one executable state-transition relation. Each realization carries an implicit constraint bias, the structural restrictions imposed by its instruction...
This work is a continuation, and generalization, of Andrew Appel's landmark work on “Compiling with Continuations”, but instead of natural-deduction-based languages like the lambda calculus, it uses sequent-calculus-inspired languages throughout all intermediate stages.
Marius Müller, David Binder, Marco Tzschentke et al.· ACM Transactions on Programm...· 0 citations
Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose rel...
Julien Simonnet, Matthieu Lemerre, Mihaela Sighireanu· Proceedings of the ACM on Pr...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
