title: Gradual Tensor Shape Checking

authors:
Momoko Hattori
Naoki Kobayashi
Ryosuke Sato

abstract: Abstract Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where users can improve the precision of the inference by adding appropriate type annotations to the program. We formalize our approach and prove that it satisfies the criteria of gradual typing proposed by Siek et al. in 2015. We have implemented a prototype shape checking tool based on our approach and evaluated its effectiveness by applying it to some deep neural network programs.


venue: esop

title: Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing

authors:
Basim Khajwal
C.-H. Luke Ong
Dominik Wagner

abstract: Abstract We study the foundations of variational inference, which frames posterior inference as an optimisation problem, for probabilistic programming. The dominant approach for optimisation in practice is stochastic gradient descent. In particular, a variant using the so-called reparameterisation gradient estimator exhibits fast convergence in a traditional statistics setting. Unfortunately, discontinuities, which are readily expressible in programming languages, can compromise the correctness of this approach. We consider a simple (higher-order, probabilistic) programming language with conditionals, and we endow our language with both a measurable and asmoothed(approximate) value semantics. We present type systems which establish technical pre-conditions. Thus we can prove stochastic gradient descent with the reparameterisation gradient estimator to be correct when applied to the smoothed problem. Besides, we can solve the original problem up to any error tolerance by choosing an accuracy coefficient suitably. Empirically we demonstrate that our approach has a similar convergence as a key competitor, but is simpler, faster, and attains orders of magnitude reduction in work-normalised variance.


title: Automated Grading of Regular Expressions

authors:
Su-Hyeon Kim
Youngwook Kim
Yo-Sub Han
Hyeonseung Im
Sang-Ki Ko

abstract: Abstract With the rapid transition to distance learning, automatic grading software becomes more important to both teachers and students. We study the problem of automatically grading the regular expressions submitted by students in courses related to automata and formal language theory. In order to utilize the semantic information of the regular expression, we define a declarative logic that can be described by regular language and at the same time has natural language characteristics, and use it for the following tasks: 1) to assign partial grades for incorrect regular expressions and 2) to provide helpful feedback to students to make them understand the reason for the grades and a way to revise the incorrect regular expressions into correct ones. We categorize the cases when students’ incorrect submissions deserve partial grades and suggest how to assign appropriate grades for each of the cases. In order to optimize the runtime complexity of the algorithm, two heuristics based on automata theory are proposed and evaluated on the dataset collected from undergraduate students. In addition, we suggest Regex2NL which translates regular expressions to natural language descriptions to give insight to students so that they can understand how the regular expressions work.


title: Interpreting Knowledge-based Programs

authors:
Alexander Knapp
Heribert Mühlberger
Bernhard Reus

abstract: Abstract Knowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.


title: Automatic Alignment in Higher-Order Probabilistic Programming Languages

authors:
Daniel Lundén
Gizem Çaylak
Fredrik Ronquist
David Broman

abstract: Abstract Probabilistic Programming Languages (PPLs) allow users to encode statistical inference problems and automatically apply an inference algorithm to solve them. Popular inference algorithms for PPLs, such as sequential Monte Carlo (SMC) and Markov chain Monte Carlo (MCMC), are built around checkpoints—relevant events for the inference algorithm during the execution of a probabilistic program. Deciding the location of checkpoints is, in current PPLs, not done optimally. To solve this problem, we present a static analysis technique that automatically determines checkpoints in programs, relieving PPL users of this task. The analysis identifies a set of checkpoints that execute in the same order in every program run—they are aligned. We formalize alignment, prove the correctness of the analysis, and implement the analysis as part of the higher-order functional PPL Miking CorePPL. By utilizing the alignment analysis, we design two novel inference algorithm variants: aligned SMC and aligned lightweight MCMC. We show, through real-world experiments, that they significantly improve inference execution time and accuracy compared to standard PPL versions of SMC and MCMC.


title: Contextual Modal Type Theory with Polymorphic Contexts

authors:
Yuito Murase
Yuichi Nishiwaki
Atsushi Igarashi

abstract: Abstract Modal types—types that are derived from proof systems of modal logic—have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts—the types of all free variables in code values. This paper presents $$\lambda _{\forall []}$$ λ ∀ [ ] , a novel extension of contextual modal type theory with parametric polymorphism over contexts. Such an extension has been studied in the literature but, unlike earlier proposals, $$\lambda _{\forall []}$$ λ ∀ [ ] is more general in that it allows multiple occurrence of context variables in a single context. We formalize $$\lambda _{\forall []}$$ λ ∀ [ ] with its type system and operational semantics given by $$\beta $$ β -reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies’ $$\lambda _{\bigcirc }$$ λ ◯ , which is based on linear-time temporal logic, to $$\lambda _{\forall []}$$ λ ∀ [ ] .


title: System Fμ ømega with Context-free Session Types

authors:
Diogo Poças
Diana Costa
Andreia Mordido
Vasco T. Vasconcelos

abstract: Abstract We study increasingly expressive type systems, from $$F^\mu $$ Fμ —an extension of the polymorphic lambda calculus with equirecursive types—to $$F^{\mu ;}_\omega $$ Fωμ; —the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of $$F^\mu _\omega $$ Fωμ as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes.


title: Safe Session-Based Concurrency with Shared Linear State

authors:
Pedro Rocha
Luís Caires

abstract: Abstract We introduce $$\textsf{CLASS}$$ CLASS , a session-typed, higher-order, core language that supports concurrent computation with shared linear state.


title: A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

authors:
Todd Schmid
Tobias Kappé
Alexandra Silva

abstract: Abstract Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa’s axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT consisting of skip-free programs.


title: Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

authors:
Michael Schwarz
Simmo Saan
Helmut Seidl
Julian Erhard
Vesal Vojdani

abstract: Abstract We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.


title: A Type System for Effect Handlers and Dynamic Labels

authors:
Paulo Emílio de Vilhena
François Pottier

abstract: Abstract We consider a simple yet expressive $$\lambda $$ λ -calculus equipped with references, effect handlers, and dynamic allocation of effect labels, and whose operational semantics does not involve coercions or rely on type information. We equip this language with a type system that supports type and effect polymorphism, allows reordering row entries and extending a row with new entries, and supports (but is not restricted to) lexically scoped handlers. This requires addressing the issue of potential aliasing between effect names. Our original solution is to interpret a row not only as a permission to perform certain effects but also as a disjointness requirement bearing on effect names. The type system guarantees strong type soundness: a well-typed program cannot crash or perform an unhandled effect. We prove this fact by encoding the type system into a novel Separation Logic for effect handlers, which we build on top of Iris. Our results are formalized in Coq.


title: Pragmatic Gradual Polymorphism with References

authors:
Wenjia Ye
Bruno C. d. S. Oliveira

abstract: Abstract Gradualizing System F has been widely discussed. A big challenge is to preserve relational parametricity and/or the gradual guarantee. Most past work has focused on the preservation of parametricity, but often without the gradual guarantee. A few recent works satisfy both properties by giving up System F syntax, or with some restrictions and the introduction of sophisticated mechanisms in the dynamic semantics. While parametricity is important for polymorphic languages, most mainstream languages typically do not satisfy it, for a variety of different reasons. In this paper, we explore the design space of polymorphic languages that satisfy the gradual guarantee, but do not preserve parametricity. When parametricity is not a goal, the design of polymorphic gradual languages can be considerably simplified. Moreover, it becomes easy to add features that are of practical importance, such as mutable references. We present a new gradually typed polymorphic calculus, called $$\lambda ^{G}_{gpr}$$ λ gpr G , with mutable references and with an easy proof of the gradual guarantee. In addition, compared to other gradual polymorphism work, $$\lambda ^{G}_{gpr}$$ λ gpr G is defined using a Type-Directed Operational Semantics (TDOS), which allows the dynamic semantics to be defined directly instead of elaborating to a target cast language. $$\lambda ^{G}_{gpr}$$ λ gpr G and all the proofs in this paper are formalized in Coq.


title: Bunched Fuzz: Sensitivity for Vector Metrics

authors:
june wunder
Arthur Azevedo de Amorim
Patrick Baillot
Marco Gaboardi

abstract: Abstract Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum. In this work, we show that these products can be generalized to arbitrary $$L^p$$ L p distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $$L^1$$ L 1 and $$L^\infty $$ L ∞ . To ease the handling of such products, we extend the Fuzz type system with bunches—as in the logic of bunched implications—where the distances of different groups of variables can be combined using different $$L^p$$ L p distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs.


title: On the Hardness of Analyzing Quantum Programs Quantitatively

authors:
Martin Avanzini
Georg Moser
Romain Péchoux
Simon Perdrix

abstract: Abstract In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction—a restriction to polynomials of bounded degree over a real closed field—we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.


title: The Session Abstract Machine

authors:
Luís Caires
Bernardo Toninho

abstract: Abstract We build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM’s design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic $$\textsf{CLL}$$ CLL . We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.


title: A Formal Treatment of Bidirectional Typing

authors:
Liang-Ting Chen
Hsiang-Shang Ko

abstract: Abstract There has been much progress in designing bidirectional type systems and associated type synthesis algorithms, but mainly on a case-by-case basis. To remedy the situation, this paper develops a general and formal theory of bidirectional typing for simply typed languages: for every signature that specifies a mode-correct bidirectionally typed language, there exists a proof-relevant type synthesiser which, given an input abstract syntax tree, constructs a typing derivation if any, gives its refutation if not, or reports that the input does not have enough type annotations. Sufficient conditions for deriving a type synthesiser such as soundness, completeness, and mode-correctness are studied universally for all signatures. We propose a preprocessing step called mode decoration, which helps the user to deal with missing type annotations. The entire theory is formally implemented in Agda, so we provide a verified generator of proof-relevant type synthesisers as a by-product of our formalism.


title: Trocq: Proof Transfer for Free, With or Without Univalence

authors:
Cyril Cohen
Enzo Crance
Assia Mahboubi

abstract: Abstract This article presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the interactive theorem prover, in the meta-language.


title: Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence

abstract: Abstract Trocq [5] is both the name of a calculus, describing a parametricity framework, and of a plugin [6] that provides tactics for performing representation changes in goals, as well as vernacular commands for specifying the expected translations.


title: Circuit Width Estimation via Effect Typing and Linear Dependency

authors:
Andrea Colledan
Ugo Dal Lago

abstract: Abstract Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.


title: A Denotational Approach to Release/Acquire Concurrency

authors:
Yotam Dvir
Ohad Kammar
Ori Lahav

abstract: Abstract We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic approach, and is based on Brookes-style traces. To do so we adapt Brookes’s traces to Kang et al.’s view-based machine for RA, and supplement Brookes’s mumble and stutter closure operations with additional operations, specific to RA. The latter provides a more nuanced understanding of traces that uncouples them from operational interrupted executions. We show that our denotational semantics is adequate and use it to validate various program transformations of interest. This is the first work to put weak memory models on the same footing as many other programming effects in Moggi’s standard monadic approach.


title: Generic bidirectional typing for dependent type theories

abstract: Abstract Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.


title: Artifact report: Generic bidirectional typing for dependent type theories

abstract: Abstract We report on the implementation of a generic bidirectional algorithm for dependent type theories, following the proposal of the paper "Generic bidirectional typing for dependent type theories".


title: Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping

authors:
Hiroya Fujinami
Ichiro Hasuo

abstract: Abstract Regular expression (regex) matching is fundamental in many applications, especially in web services. However, matching by backtracking—preferred by most real-world implementations for its practical performance and backward compatibility—can suffer from so-called catastrophic backtracking, which makes the number of backtracking super-linear and leads to the well-known ReDoS vulnerability. Inspired by a recent algorithm by Davis et al. that runs in linear time for (non-extended) regexes, we study efficient backtracking matching for regexes with two common extensions, namely look-around and atomic grouping. We present linear-time backtracking matching algorithms for these extended regexes. Their efficiency relies on memoization, much like the one by Davis et al.; we also strive for smaller memoization tables by carefully trimming their range. Our experiments—we used some real-world regexes with the aforementioned extensions—confirm the performance advantage of our algorithms.


title: Monadic Intersection Types, Relationally

authors:
Francesco Gavazzo
Riccardo Treglia
Gabriele Vanoni

abstract: Abstract We extend intersection types to a computational $$\lambda $$ λ -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics, but also in the type system . Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.


title: Higher-Order LCTRSs and Their Termination

authors:
Liye Guo
Cynthia Kop

abstract: Abstract Logically constrained term rewriting systems (LCTRSs) are a formalism for program analysis with support for data types that are not (co)inductively defined. Only imperative programs have been considered through the lens of LCTRSs so far since LCTRSs were introduced as a first-order formalism. In this paper, we propose logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order generalization of LCTRSs, which suits the needs of representing and analyzing functional programs. We also study the termination problem of LCSTRSs and define a variant of the higher-order recursive path ordering (HORPO) for the newly proposed formalism.


title: Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis

authors:
Jason Z. S. Hu
Brigitte Pientka

abstract: Abstract We introduce layering to modal type theory to combine type theory with intensional analysis. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed $$\lambda $$ λ -calculus with no modality. Layer 1 is obtained by extending the core language with one layer of contextual $$\square $$ □ types to support pattern matching on potentially open code from layer 0 while retaining normalization. Although both layers fundamentally share the same language and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda. Layered modal type theory provides a uniform foundation for meta-programming with intensional analysis. We see this work as an important step towards a foundational way to support meta-programming in proof assistants.


title: Program Synthesis from Graded Types

authors:
Jack Hughes
Dominic Orchard

abstract: Abstract Graded type systems are a class of type system for fine-grained quantitative reasoning about data-flow in programs. Through the use of resource annotations (or grades), a programmer can express various program properties at the type level, reducing the number of typeable programs. These additional constraints on types lend themselves naturally to type-directed program synthesis, where this information can be exploited to constrain the search space of programs. We present a synthesis algorithm for a graded type system, where grades form an arbitrary pre-ordered semiring. Harnessing this grade information in synthesis is non-trivial, and we explore some of the issues involved in designing and implementing a resource-aware program synthesis tool. In our evaluation we show that by harnessing grades in synthesis, the majority of our benchmark programs (many of which involve recursive functions over recursive ADTs) require less exploration of the synthesis search space than a purely type-driven approach and with fewer needed input-output examples. This type-and-graded-directed approach is demonstrated for the research language Granule but we also adapt it for synthesising Haskell programs that use GHC’s linear types extension.


title: Hyperproperty Verification as CHC Satisfiability

authors:
Shachar Itzhaky
Sharon Shoham
Yakir Vizel

abstract: Abstract Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a total alignment of different executions that facilitates simpler inductive invariants. We show how this treatment is achieved via a reduction from the verification problem of $$\forall ^*\exists ^*$$ ∀ ∗ ∃ ∗ hyperproperties to Constrained Horn Clauses (CHCs). Our starting point is a set of universally quantified formulas in first-order logic (modulo theories) that encode the verification of $$\forall ^*\exists ^*$$ ∀ ∗ ∃ ∗ hyperproperties over infinite-state transition systems. The first-order encoding uses uninterpreted predicates to capture the (1) witness function for existential quantification over traces, (2) alignment of executions, and (3) corresponding inductive invariant. Such an encoding was previously proposed for k-safety properties. Unfortunately, finding a satisfying model for the resulting first-order formulas is beyond reach for modern first-order satisfiability solvers. Previous works tackled this obstacle by developing specialized solvers for the aforementioned first-order formulas. In contrast, we show that the same problems can be encoded as CHCs and solved by existing CHC solvers. CHC solvers take advantage of the unique structure of CHC formulas and handle the combination of quantifiers with theories and uninterpreted predicates more efficiently. Our key technical contribution is a logical transformation of the aforementioned sets of first-order formulas to equi-satisfiable sets of CHCs. The transformation to CHCs is sound and complete, and applying it to the first-order formulas that encode verification of hyperproperties leads to a CHC encoding of these problems. We implemented the CHC encoding in a prototype tool and show that, using existing CHC solvers for solving the CHCs, the approach already outperforms state-of-the-art tools for hyperproperty verification by orders of magnitude.


title: Verified Inlining and Specialisation for PureCake

authors:
Hrutvik Kanabar
Kacper Korban
Magnus O. Myreen

abstract: Abstract Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programming language. A novel aspect of our formalisation is that we justify inlining by pushing and pulling "Image missing"-bindings. All of our work has been mechanised in the HOL4 interactive theorem prover.


title: A Modular Soundness Theory for the Blackboard Analysis Architecture

authors:
Sven Keidel
Dominik Helm
Tobias Roth
Mira Mezini

abstract: Abstract Sound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program semantics (the static and the dynamic semantics) which are hard to reason about. Second, the more the static and dynamic semantics differ, the more work a soundness proof needs to do to bridge the impedance mismatch. These problems increase the effort and complexity of soundness proofs. Existing soundness theories address these problems by deriving both the dynamic and static semantics from the same artifact, often called generic interpreter. A generic interpreter provides a common structure along which a soundness proof can be composed, which avoids having to reason about the analysis as a whole. However, a generic interpreter restricts which analyses can be derived, as all derived analyses must roughly follow the program execution order. To lift this restriction, we develop a soundness theory for the blackboard analysis architecture, which is capable of describing backward, demand-driven, and summary-based analyses. The architecture describes static analyses with small independent modules, which communicate via a central store. Soundness of a compound analysis follows from soundness of all of its modules. Furthermore, modules can be proven sound independently, even though modules depend on each other. We evaluate our theory by proving soundness of four analyses: a pointer and call-graph analysis, a reflection analysis, an immutability analysis, and a demand-driven reaching definitions analysis.


title: Definitional Functoriality for Dependent (Sub)Types

authors:
Théo Laurent
Meven Lennon-Bertrand
Kenji Maillard

abstract: Abstract Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations satisfied propositionally by a large class of container-like type constructors $$F : {\text {Type}}\rightarrow {\text {Type}}$$ F : Type → Type , equipped with a $$\textrm{map}_{F} {{\,\mathrm{:}\,}}(A \rightarrow B) \rightarrow F\,A \rightarrow F\,B$$ map F : ( A → B ) → F A → F B , such as lists or trees. Promoting these equations to definitional ones strengthens the theory, enabling slicker proofs and more automation for functorial type constructors. This extension is used to modularly justify a structural form of coercive subtyping, propagating subtyping through type formers in a map-like fashion. We show that the resulting notion of coercive subtyping, thanks to the extra definitional equations, is equivalent to a natural and implicit form of subsumptive subtyping. The key result of decidability of type-checking in a dependent type system with functor laws for lists has been entirely mechanized in Coq.


title: Artifact Description - Definitional Functoriality for Dependent (Sub)Types

abstract: Abstract This document describes the Coq formalisation accompanying the paper Definitional Functoriality for Dependent (Sub)Types, more specifically the content of section 4.


title: Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation

authors:
Pierre Lermusiaux
Benoît Montagu

abstract: Abstract Exception handling is a key feature in modern programming languages. Exceptions can be used to deal with errors, or as a means to control the flow of execution of a program. Since they might unexpectedly terminate a program, unhandled exceptions are a serious safety concern. We propose a static analysis to detect uncaught exceptions in functional programs, that is defined as an abstract interpreter. It computes a description of the values potentially returned by a program using a novel abstract domain, that can express inductively defined sets of values. Simultaneously, the analysis infers the possibly raised exceptions, by computing in theabstract exception monad. This abstract interpreter has been implemented as an effective static analyser for a large subset of programs, that supports mutable data types, the module system, and dynamically extensible data types such as the exception type. The analyser has been evaluated on several hundreds of programs.


title: Deciding Subtyping for Asynchronous Multiparty Sessions

authors:
Elaine Li
Felix Stutz
Thomas Wies

abstract: Abstract Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as implementation model. We address two problems: when can a local implementation safely substitute another, and when does an arbitrary CSM implement a global type? We define safety with respect to a given global type, in terms of subprotocol fidelity and deadlock freedom. Our implementation model subsumes existing work which considers local types with restricted choice. We exploit the connection between MST subtyping and refinement to formulate concise conditions that are directly checkable on the candidate implementations, and use them to show that both problems are decidable in polynomial time.


title: Scoped Effects as Parameterized Algebraic Theories

authors:
Sam Lindley
Cristina Matache
Sean K. Moss
Sam Staton
Nicolas Wu
Zhixuan Yang

abstract: Abstract Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories. We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our fresh perspective by way of equational characterizations of several known models of scoped effects.


title: Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages

authors:
Daniel Lundén
Lars Hummelgren
Jan Kudlicka
Oscar Eriksson
David Broman

abstract: Abstract Universal probabilistic programming languages (PPLs) make it relatively easy to encode and automatically solve statistical inference problems. To solve inference problems, PPL implementations often apply Monte Carlo inference algorithms that rely on execution suspension. State-of-the-art solutions enable execution suspension either through (i) continuation-passing style (CPS) transformations or (ii) efficient, but comparatively complex, low-level solutions that are often not available in high-level languages. CPS transformations introduce overhead due to unnecessary closure allocations—a problem the PPL community has generally overlooked. To reduce overhead, we develop a new efficient selective CPS approach for PPLs. Specifically, we design a novel static suspension analysis technique that determines parts of programs that require suspension, given a particular inference algorithm. The analysis allows selectively CPS transforming the program only where necessary. We formally prove the correctness of the analysis and implement the analysis and transformation in the Miking CorePPL compiler. We evaluate the implementation for a large number of Monte Carlo inference algorithms on real-world models from phylogenetics, epidemiology, and topic modeling. The evaluation results demonstrate significant improvements across all models and inference algorithms.


title: Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

authors:
Raphaël Monat
Aymeric Fromherz
Denis Merigoux

abstract: Abstract Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users. In this work, we aim to provide a solid foundation for date arithmetic working on days, months and years. We first present a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F $$^\star $$ ⋆ proof assistant. Building upon this semantics, we then propose a static analysis by abstract interpretation to automatically detect ambiguities in date computations. We finally integrate our approach in the Catala language, a recent domain-specific language for formalizing computational law, and use it to analyze the Catala implementation of the French housing benefits, leading to the discovery of several date-related ambiguities.


title: Maximal Quantified Precondition Synthesis for Linear Array Loops

authors:
Sumanth Prabhu
Grigory Fedyukovich
Deepak D'Souza

abstract: Abstract Precondition inference is an important problem with many applications in verification and testing. Finding preconditions can be tricky as programs often have loops and arrays, which necessitates finding quantified inductive invariants. However, existing techniques have limitations in finding such invariants, especially when preconditions are missing. Further, maximal (or weakest) preconditions are often required to maximize the usefulness of preconditions. So the inferred inductive invariants have to be adequately weak. To address these challenges, we present an approach for maximal quantified precondition inference using aninfer-check-weakenframework. Preconditions and inductive invariants are inferred by a novel technique calledrange abduction, and then checked for maximality and weakened if required. Range abduction attempts to propagate the given quantified postcondition backwards and then strengthen or weaken it as needed to establish inductiveness. Weakening is done in a syntax-guided fashion. Our evaluation performed on a set of public benchmarks demonstrates that the technique significantly outperforms existing techniques in finding maximal preconditions and inductive invariants.


title: Observational Equality Meets CIC

authors:
Loïc Pujet
Nicolas Tabareau

abstract: Abstract Equality is at the heart of dependent type theory, as it plays a fundamental role in specifications and mathematical reasoning. The standard way to handle it in mainstream proof assistants such as Agda, Lean or Coq is based on Martin-Löf’s identity type, which comes straight out of the ’70s—its elegance and simplicity have earned it a long-standing use, despite a major discrepancy with traditional mathematical formulations: it does not satisfy any extensionality principles. Recently, the work on observational equality has regained interest as a new way to encode equality in proof assistants that support a universe of definitionally proof-irrelevant propositions; however it has yet to be integrated in any major proof assistant, because it is not fully compatible with another important feature of type theory: indexed inductive types. In this paper, we propose a systematic integration of indexed inductive types with an observational equality, and show that this integration can only be completely satisfactory if the observational equality satisfies the computational rule of Martin-Löf’s identity type. The second contribution of this paper is a formal proof that this additional computation rule, although not present in previous works on observational equality, can be integrated to the system without compromising the decidability of conversion.


title: Intel PMDK Transactions: Specification, Validation and Concurrency

authors:
Azalea Raad
Ori Lahav
John Wickerson
Piotr Balcer
Brijesh Dongol

abstract: Abstract Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of byte-addressable persistent memory, a natural question to ask is whether STM systems can be adapted to support failure atomicity. In this paper, we answer this question by showing how STM can be easily integrated with Intel’s Persistent Memory Development Kit (PMDK) transactional library (which we refer to as txPMDK) to obtain STM systems that are both concurrent and persistent. We demonstrate this approach using known STM systems, TML and NOrec, which when combined with txPMDK result in persistent STM systems, referred to as PMDK-TML and PMDK-NORec, respectively. However, it turns out that existing correctness criteria are insufficient for specifying the behaviour of txPMDK and our concurrent extensions. We therefore develop a new correctness criterion, dynamic durable opacity, that extends the previously defined notion of durable opacity with dynamic memory allocation. We provide a model of txPMDK, then show that this model satisfies dynamic durable opacity. Moreover, dynamic durable opacity supports concurrent transactions, thus we also use it to show correctness of both PMDK-TML and PMDK-NORec.


title: Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency

abstract: Abstract This report extends §6 of the main paper by providing further details of the mechanisation effort.


title: Specifying and Verifying Persistent Libraries

authors:
Léo Stefanesco
Azalea Raad
Viktor Vafeiadis

abstract: Abstract We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the and libraries, verify their implementations over "Image missing", and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.


title: Reconciling Partial and Local Invertibility

authors:
Anders Ågren Thuné
Kazutaka Matsuda
Meng Wang

abstract: Abstract Invertible programming languages specify transformations to be run in two directions, such as compression/decompression or encryption/decryption. Two key concepts in invertible programming languages are partial invertibility and local invertibility. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing. We find that existing approaches lack a satisfying treatment of partial invertibility, leaving the connection to local invertibility unclear. In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language Kalpis, and show how to give them a locally invertible semantics using the novel arrow combinator language $$\textsc {rrArr}$$ R R A R R —the key idea is viewing partial invertibility as an invertible effect. By formalizing the two systems and giving Kalpis semantics by translation to $$\textsc {rrArr}$$ R R A R R , we reconcile partial and local invertibility, solving an open problem in the field. All formal developments are mechanized in Agda.


title: The Vanilla Sequent Calculus is Call-by-Value

abstract: 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 that call-by-value was introduced in an intuitionistic setting without linear features. This paper shows that the most basic sequent calculus for minimal intuitionistic logic—dubbed here vanilla—can naturally be seen as a logical interpretation of call-by-value evaluation. This is obtained by establishing mutual simulations with a well-known formalism for call-by-value evaluation.


title: Formulas as Processes, Deadlock-Freedom as Choreographies

authors:
Matteo Acclavio
Giulia Manara
Fabrizio Montesi

abstract: 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 of the recursion-free $$\pi $$ π -calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the $$\pi $$ π -calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite $$\pi $$ π -calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the $$\pi $$ π -calculus, and the expressiveness of choreographic languages.


title: Sufficient Conditions for Robustness of RDMA Programs

authors:
Guillaume Ambal
Ori Lahav
Azalea Raad

abstract: 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 addresses the challenge of establishing sufficient conditions for RDMA robustness. We introduce a set of straightforward criteria that, when met, guarantee sequential consistency and mitigate potential issues arising from weak memory behaviours in RDMA applications. Notably, when restricted to a tree topology, these conditions become even more relaxed, significantly reducing the need for synchronisation primitives. This work provides developers with practical guidelines to ensure the reliability and correctness of their RDMA-based systems.


title: Constructive characterisations of the MUST-preorder for asynchrony

authors:
Giovanni Bernardi
Ilaria Castellani
Paul Laforgue
Léo Stefanesco

abstract: 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 clients, this definition does not yield a practical proof method, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions. We show that the standard characterisations of the $$\textsc {must}$$ M U S T -preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Coq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous $$\pi $$ π -calculus. We show that the standard coinductive characterisation lets us prove in Coq that concrete programs are related by the $$\textsc {must}$$ M U S T -preorder. Finally, our proofs show that Brouwer’s bar induction principle is a useful technique to reason on liveness preserving program transformations.


title: Abstraction of memory block manipulations by symbolic loop folding

authors:
Jérôme Boillot
Jérôme Feret

abstract: 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 properties consist of equalities and comparison predicates involving abstract expressions, represented as affine forms in the loop counters and symbolic dereferences. All these methods have been incorporated within the © static analyzer that checks for the absence of run-time errors in embedded critical software. We also give insights on how to implement this abstract domain within any other C static analyzer.


title: Cognacy Queries over Dependence Graphs for Transparent Visualisations

authors:
Joseph Bond
Cristina David
Minh Nguyen
Dominic Orchard
Roly Perera

abstract: 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 significant challenge. We introduce a new program analysis framework (A supporting artifact is available at https://zenodo.org/records/14637654 [5].) which supports interactive exploration of fine-grained IO relationships directly through computed outputs, using dynamic dependence graphs. This framework enables a novel notion in data provenance which we call linked inputs, a relation of mutual relevance or cognacy which arises between inputs that contribute to common features of the output. We give a procedure for computing linked inputs over a dependence graph, and show how the presented in this paper is faster on most examples than an implementation based on execution traces.


title: An abstract, certified account of operational game semantics

authors:
Peio Borthelle
Tom Hirschowitz
Guilhem Jaber
Yannick Zakowski

abstract: 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 programs, weak bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs. In this paper, we contribute to the unification and mechanisation of OGS. Indeed, we propose an abstract notion of language with evaluator, for which we construct a generic OGS interpretation, which we prove sound. Our framework covers a variety of simply-typed and untyped lambda-calculi with various evaluation strategies. These calculi notably feature recursive definitions, first-class continuations, and a wide variety of datatypes. All constructions and proofs are entirely mechanised in the Coq proof assistant.


title: Artifact Report: an Abstract, Certified Account of Operational Game Semantics

abstract: 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 Operational Game Semantics (OGS). All our results are mechanised in the Coq proof assistant: this mechanisation (The proof artifact is archived at https://doi.org/10.5281/zenodo.14697618 .) constitutes the artifact we discuss in the present document. More specifically, our mechanisation covers our main result, the soundness of the abstract OGS model w.r.t. substitution equivalence (Theorem 8), as well as four example calculi: two variants of call-by-value $$\lambda $$ λ -calculus and two variants of $$\mu \tilde{\mu }$$ μ μ ~ -calculus [4, 5]. The only axiom used is the Axiom K [17] for equality proof irrelevance (To ease dependent pattern matching due to the intrinsically scoped representation.). The explains the installation process and the structure of the code. An online rendering ( https://lapin0t.github.io/ogs/esop25/Readme.html .) is available thanks to Alectryon [12]. Furthermore, the main paper provides systematic hyperlinks from statements to their Coq counterparts. We encourage the interested reader to use these tools to navigate the code. In this document, we focus first on users: how to read and instantiate our main result. We then detail salient technical aspects of our mechanisation.


title: Multiparty Session Types with a Bang!

authors:
Matthew Alan Le Brun
Simon Fowler
Ornela Dardha

abstract: 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-passing programs. We introduce $$\textsf {MPST!} $$ MPST ! , a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of $$\textsf {MPST!} $$ MPST ! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.


title: Stratified Type Theory

authors:
Jonathan Chan
Stephanie Weirich

abstract: 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 the only option for universes in type theory. Taking inspiration from Leivant’s Stratified System F, we introduce Stratified Type Theory (), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In , we consider a number of extensions beyond just stratified dependent functions. First, the subsystem employs McBride’s crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full includes a separate nondependent function type with a floating domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven to be consistent and to be type safe, but consistency of the full remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe to be consistent, and as evidence have verified the ill-typedness of some well-known type-theoretic paradoxes using our implementation.


title: Neural Network Verification is a Programming Language Challenge

authors:
Lucas C. Cordeiro
Matthew L. Daggitt
Julien Girard-Satabin
Omri Isac
Taylor T. Johnson
Guy Katz
Ekaterina Komendantskaya
Augustin Lemesle
Edoardo Manino
Artjoms Sinkarovs
Haoze Wu

abstract: 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 unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.


title: Variable Elimination as Rewriting in a Linear Lambda Calculus

authors:
Thomas Ehrhard
Claudia Faggian
Michele Pagani

abstract: 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 Elimination as an algorithm acting on programs in an idealized probabilistic functional language—a linear simply-typed $$\lambda $$ λ -calculus suffices for our purpose. Precisely, we express $$\textsf{VE}$$ VE as a term rewriting process, which transforms a global definition of a variable into a local definition, by swapping and nesting let-in expressions. We exploit in an essential way linear types.


title: Coverage Semantics for Dependent Pattern Matching

authors:
Joseph Eremondi
Ohad Kammar

abstract: 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 to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns. This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.


title: A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model

authors:
Weijie Fan
Hongjin Liang
Xinyu Feng
Hanru Jiang

abstract: 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-local verification. With a novel “split” mechanism, one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us to avoid considering different execution paths of branch statements simultaneously. The logic rules are compositional and are natural extensions of their sequential counterparts. Using our program logic, we verify four typical algorithms in the oblivious adversary model.


title: Iso-Recursive Multiparty Sessions and their Automated Verification

authors:
Marco Giunti
Nobuko Yoshida

abstract: 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 multiparty session types (GMST). In GMST, in order to establish properties as deadlock-freedom, the environments which type processes are assumed to satisfy extensional properties holding in all infinite sequences. This is a problem because: (1) the mechanisation of GMST and equi-recursion in proof assistants is utterly complex and eventually requires co-induction; and (2) the implementation of GMST in type checkers relies on model checkers for environment verification, and thus the program analysis is not self-contained. In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.


title: Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences

authors:
Amir Kafshdar Goharshady
S. Hitarth
Sergei Novozhilov

abstract: Abstract Recurrence relations are used in a wide variety of static program analysis tasks such as loop summarization, invariant generation, and, most classically, modeling the (asymptotic) worst-case runtime behavior of recursive divide-and-conquer algorithms. In this work, we focus on the latter use-case. Classical methods for this problem, such as the well-known Master Theorem (MT) or the Akra-Bazzi method (AB) can only handle single recurrences of a certain limited form. Specifically, MT requires that each instance be divided into a fixed number of smaller sub-instances of the same size. AB generalizes MT by allowing sub-instances of different sizes, but still requires that the number of such sub-instances be fixed and independent of the size of the original instance. Moreover, these methods can handle neither multi-variate recurrences nor systems of recurrences that model non-simple recursive behavior among two or more procedures. In this work, we lift these restrictions and consider a wide family of recurrences called Generalized Polynomial Recurrence Systems (GPRS). Our setting is highly expressive and allows systems of multi-variate recurrences in which an instance can be divided into polynomially-many sub-instances. Moreover, the division is not limited to a single rule and can have several cases based on conditions on the values of the variables. We show how to obtain polynomial upper-bounds for a GPRS using template-based methods and classical theorems from polyhedral and algebraic geometry. Our approach reduces the synthesis of polynomial upper-bounds to linear or semi-definite programming instances, enabling efficient solutions. Crucially, our method is sound and semi-complete, i.e. complete for polynomials of any fixed degree and obtains concrete, as opposed to asymptotic, upper-bounds.


title: CUTECat: Concolic Execution for Computational Law

authors:
Pierre Goutagny
Aymeric Fromherz
Raphaël Monat

abstract: Abstract Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs intended to faithfully transcribe the law into computer code. Bugs in these programs can lead to dramatic societal impact, e.g., paying employees incorrect amounts, or not awarding benefits to families in need. To address this issue, we consider concolic unit testing, a combination of concrete execution with SMT-based symbolic execution, and propose CUTECat, a concolic execution tool targeting implementations of computational laws. Such laws typically follow a pattern where a base case is later refined by many exceptions in following law articles, a pattern that can be formally modeled using default logic. We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala, a recent domain-specific language tailored to implement computational laws. We evaluate CUTECat on several programs, including the Catala implementation of the French housing benefits and Section 132 of the US tax code. We show that CUTECat can successfully generate hundreds of thousands of testcases covering all branches of these bodies of law. Through several heuristics, we improve CUTECat’s scalability and usability, making the testcases understandable by lawyers and programmers alike. We believe CUTECat paves the way for the use of formal methods during legislative processes.


title: First-Person Choreographic Programming with Continuation-Passing Communications

abstract: Abstract Choreographic programming (CP) is a method to implement distributed systems that ensures communication deadlock freedom by design. To use CP, though, the number of processes and the network among them must be known statically. Often, that information is known only dynamically. Thus, existing CP languages cannot be used to implement process-parametric distributed systems. This paper introduces first-person choreographic programming (1CP) to support the implementation of process-parametric distributed systems while also ensuring communication deadlock freedom. We present both a design of 1CP (new calculus, formalised in Isabelle/HOL) and an implementation (new language and tooling, integrated in VS Code).

awards:
Distinguished Paper
EAPLS Best Paper


title: Verifying Algorithmic Versions of the Lovász Local Lemma

authors:
Rongen Lin
Hongjin Liang
Xinyu Feng

abstract: Abstract Algorithmic versions of the Lovász Local Lemma (ALLLs), or rather, the Moser-Tardos algorithm and its variants, are impactful in both theory and practice. In this paper, we take the first step towards the goal of formally verifying ALLLs by applying programming language techniques. We propose two proof recipes, called loop truncation and resampling-table-based coupling, for bridging the gap between Hoare-style program logics and ALLLs’ original informal proofs. We formally verify six existing important results related to ALLLs, and propose a new result which generalizes several existing results. Our proof recipes can also be used to verify general properties of other probabilistic programs in addition to ALLLs.


title: Formal Autograding in a Classroom

authors:
Dragana Milovancevic
Mario Bucev
Marcin Wojnarowski
Samuel Chassot
Viktor Kuncak

abstract: Abstract We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiment, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We were able to use program equivalence to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input-output behaviour is identical. Consequently, we achieve (1) higher confidence in correctness of idiomatic solutions but also (2) more thorough assessment of solution landscape that reveals solutions beyond those envisioned by instructors.


title: coma, an Intermediate Verification Language with Explicit Abstraction Barriers

authors:
Andrei Paskevich
Paul Patault
Jean-Christophe Filliâtre

abstract: International audience


title: A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming

authors:
Robin Piedeleu
Mateo Torres-Ruiz
Alexandra Silva
Fabio Zanasi

abstract: Abstract We introduce a sound and complete equational theory capturing equivalence of discrete probabilistic programs, that is, programs extended with primitives for Bernoulli distributions and conditioning, to model distributions over finite sets of events. To do so, we translate these programs into a graphical syntax of probabilistic circuits, formalised as string diagrams, the two-dimensional syntax of symmetric monoidal categories. We then prove a first completeness result for the equational theory of the conditioning-free fragment of our syntax. Finally, we extend this result to a complete equational theory for the entire language. Our first result gives a presentation of the category of Markov kernels, restricted to objects that are powers of the two-elements set.


title: Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

authors:
Florian Sextl
Adam Rogalewicz
Tomás Vojnar
Florian Zuleger

abstract: Abstract Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation. This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques; both in terms of precision and runtime of the analysis.


title: SMT-Boosted Security Types for Low-Level MPC

authors:
Christian Skalka
Joseph P. Near

abstract: Abstract Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written in the Prelude/Overture language framework. Judgements in the type theory are predicated on SMT verifications in a theory of finite fields, which supports precise and efficient analysis. Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.


title: Formal Verification of WTO-based Dataflow Solvers

authors:
Roméo La Spina
Delphine Demange
Sandrine Blazy

abstract: Abstract In this paper, we consider specific dataflow solvers, inspired by the work of Bourdoncle [5], in which an iteration order is pre-computed, based on the structure of the control-flow graph of programs. Our work aims at a clearer formulation and a better understanding of the folklore algorithms proposed three decades ago. We present a formalization of the dataflow solvers. Central to the proof of correctness is the general notion of a Weak Topological Ordering (WTO). Our correctness proofs are valid for any such ordering. The first solver implements an iterative strategy over the ordering, the second solver implements a recursive strategy. Our formalization is done within the Coq proof assistant and our solvers are extractable to OCaml code. Our formalization is fully compatible with the interface of dataflow solvers of the verified, optimizing C CompCert compiler. We conduct practical experiments on the wide range of forward and backward analyses of CompCert, demonstrating the practicality of our solvers in terms of efficiency and precision.


title: Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report

abstract: Abstract In this report, we provide our full set of results for the experimental evaluation of our formally verified, WTO-based dataflow solvers [2]. We also detail useful information regarding our artifact [3] and evaluation setup. In particular, we validate experimentally that our implementation of Bourdoncle’s iteration strategies have acceptable performances in practice, when applied to the dataflow analyses used in the CompCert C verified compiler. Our experiments also help better understanding the differences between the solvers, their strengths and their weaknesses.


title: Context-Dependent Effects in Guarded Interaction Trees

authors:
Sergei Stepanenko
Emma Nardino
Dan Frumin
Amin Timany
Lars Birkedal

abstract: Abstract Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., , and . Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called “bind rule” in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.


title: An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols

authors:
Felix Stutz
Emanuele D'Osualdo

abstract: Abstract We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a $$\pi $$ π -calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called “tame”, for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).


title: Named Arguments as Intersections, Optional Arguments as Unions

authors:
Yaozhu Sun
Bruno C. d. S. Oliveira

abstract: Abstract Named and optional arguments are prevalent features in many mainstream programming languages, enhancing code readability and flexibility. Despite widespread use, their formalization has not been extensively studied. This paper bridges this gap by presenting a type-safe foundation for named and optional arguments using intersection and union types. We begin by identifying a critical type-safety issue in popular static type checkers for Python and Ruby, particularly in handling first-class named arguments in the presence of subtyping. Our solution involves rewriting call sites to ensure type safety, which we formalize through a translation into a core calculus called $$\lambda _\textsf{iu}$$ λ iu . The type safety of the translation is proven using the Coq proof assistant. The practical implementation of our approach in the CP language validates our theoretical contributions. Furthermore, we informally discuss how our approach could be adapted to encode named and optional arguments in other existing languages.


title: Context-Sensitive Demand-Driven Control-Flow Analysis

authors:
Tim Whiting
Kimball Germane

abstract: Abstract By decoupling and decomposing control flows, demand control-flow analysis (CFA) resolves only the flow segments determined necessary to produce a specified control-flow fact. It therefore presents a more flexible interface and pricing model than typical CFA, making many useful applications practical. At present, the only realization of demand CFA is the context-insensitive Demand 0CFA. Typical mechanisms for adding context sensitivity are not compatible with the demand setting because the analyzer is dispatched at arbitrary program points in indeterminate contexts. We overcome this challenge by identifying a context suitable for a demand analysis and designing a representation thereof that allows it to model incomplete knowledge of the context. On top of this design, we construct Demand m-CFA, a context-sensitive demand CFA hierarchy. With the attractive pricing model of demand analysis and the precision offered by context sensitivity, we show that Demand m-CFA can replace its exhaustive counterpart in compiler backends and integrate into interactive tools such as language servers.


title: On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic

authors:
Risa Yamada
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato

abstract: Abstract We study the relationship between two approaches to higher-order program verification: a semi-automated method using Dijkstra monads and a fully automated method using a higher-order fixpoint logic called HFL(Z). Although the origins of both approaches are quite different, there are some striking similarities: both convert programs to corresponding predicate transformers, and the conversion is essentially obtained by a CPS transformation. After reviewing the two approaches, we formalize an exact correspondence between the two for a restricted fragment of a functional language. We also point out that, outside the restricted fragment, there are some important differences between the two approaches, suggesting the need for cross-fertilization to obtain the best of the two approaches. As an example of the cross-fertilization, we also propose a semi-automated verification method, which requires less annotations than the Dijkstra monad approach and can scale to larger programs than the HFL(Z) approach.


title: Elucidating Type Conversions in SQL Engines

authors:
Wenjia Ye
Matías Toro
Claudio Gutierrez
Bruno C. d. S. Oliveira
Éric Tanter

abstract: Abstract Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts of SQL, directly affect the portability of queries between engines. To understand this problem, we present a formal typing semantics for SQL, named $$\textsf{TRAF} $$ TRAF , that explicitly captures both static and dynamic type behavior. The system $$\textsf{TRAF} $$ TRAF is expressed in terms of abstract operators that provide the necessary leeway to precisely model different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees regarding the handling of types. We provide practical conditions on engines to prove type safety and soundness of queries. In this regard, $$\textsf{TRAF} $$ TRAF can serve as precise documentation of typing in existing engines and potentially guide their evolution, as well as provide a formal basis to study type-aware query optimizations, and design provably-correct query translators. Additionally, we test the adequacy of the formalism, implementing $$\textsf{TRAF} $$ TRAF in Python for these five engines, and tested them with thousands of randomly-generated queries.


title: Specifying and Verifying RDMA Synchronisation

authors:
Guillaume Ambal
Max Stupple
Brijesh Dongol
Azalea Raad

abstract: Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring correctness of RDMA programs has only recently become possible with the formalisation of rdmatso semantics (describing the behaviour of RDMA networking over a TSO CPU). However, this semantics currently lacks a formalisation of remote synchronisation, meaning that the implementations of common abstractions such as locks cannot be verified. In this paper, we close this gap by presenting $$\textsc {rdma}^{\textsc {tso}}_{\textsc {rmw}}$$ , the first semantics for remote ‘read-modify-write’ (RMW) instructions over TSO. It turns out that remote RMW operations are weak and only ensure atomicity against other remote RMWs. We therefore build a set of composable synchronisation abstractions starting with the $$\textsc {rdma}^{\textsc {wait}}_{\textsc {rmw}}$$ library. Underpinned by $$\textsc {rdma}^{\textsc {wait}}_{\textsc {rmw}}$$ , we then specify, implement and verify three classes of remote locks that are suitable for different scenarios. Additionally, we develop the notion of a strong RDMA model, $$\textsc {rdma}^{\textsc {sc}}_{\textsc {rmw}}$$ , which is akin to sequential consistency in shared memory architectures. Our libraries are built to be compatible with an existing set of high-performance libraries called loco, which ensures compositionality and verifiability.


title: Contextual Metaprogramming for Session Types

authors:
Pedro Ângelo
Atsushi Igarashi
Yuito Murase
Vasco T. Vasconcelos

abstract: We propose the integration of staged metaprogramming into a session-typed message passing functional language. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may be boxed and transmitted in messages. Once received, one such value may then be unboxed and locally applied before being run. To motivate this integration, we present examples of real-world use cases, for which our system would be suitable, such as servers preparing and shipping code on demand via session typed messages. We present a type system that distinguishes linear (used exactly once) from unrestricted (used an unbounded number of times) resources, and further define a type checker, suitable for a concrete implementation. We show type preservation, a progress result for sequential computations and absence of runtime errors for the concurrent runtime environment, as well as the correctness of the type checker.


title: In Cantor Space No One Can Hear You Stream

authors:
Martin Baillon
Assia Mahboubi
Pierre-Marie Pédrot

abstract: Abstract We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of $$\textsf{MLTT}$$ MLTT , we show that they inductively approximate idealized functional objects as decision trees, realizing a generalized form of continuity. We materialize this intuition in $$\textsf{MLTT}^{\textsf{F}}$$ MLTT F , a case-study sheaf extension of $$\textsf{MLTT}$$ MLTT with a Cohen real and leverage it to show uniform continuity of all $$\textsf{MLTT}$$ MLTT functionals of type $$({\mathbb {N}}\rightarrow {\mathbb {B}}) \rightarrow {\mathbb {N}}$$ ( N → B ) → N . The latter results were mechanized in Rocq.


title: Deciding not to Decide - Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism

authors:
Patrycja Balik
Szymon Jedras
Piotr Polesiuk

abstract: Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect systems did not yet gain widespread adoption. One reason for this is that type-and-effect systems are more complex and the existing inference algorithms make compromises between expressiveness, intuitiveness, and decidability. In this work, we present an effect inference algorithm for a type-and-effect system with subtyping, expressive higher-rank polymorphism, and intuitive set-like semantics of effects. In order to deal with scoping issues of higher-rank polymorphism, we delay solving of effect constraints by transforming them into formulae of propositional logic. We prove soundness and completeness of our algorithm with respect to a declarative type-and-effect system. All the presented results have been formalized in the Rocq proof assistant, and the algorithm has been successfully used in the implementation of the Fram programming language.


title: Recursive Logical Relations for Intuitionistic Linear Logic Session Types

authors:
Stephanie Balzer
Farzaneh Derakhshan
Robert Harper
Yue Yao

abstract: Abstract Program equivalence is the heart of reasoning about and proving properties of programs. To assert noninterference, for example, a program is shown to be equivalent to itself up to the confidentiality level of an observer. A powerful enabler for such proofs are logical relations , which, guided by the type structure, prescribe when two programs are indistinguishable. Logical relations enjoy ample exploration in functional languages, including languages with general recursion and a higher-order store—yet logical relations for session types only exist for terminating languages. This paper scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive equivalence for intuitionistic linear logic session types , tackling the challenges non-termination and concurrency pose. In particular, the relation only equates a diverging program with another diverging one and accounts for nondeterminism of scheduling. The logical relation has two distinguishing characteristics: it is (i) indexed with an intuitionistic linear sequent , validating cut reductions and affording biorthogonal closure , and (ii) bound by an observation index , stratifying the logical relation in the presence of recursion. Biorthogonal closure validates the logical relation, proving that the induced equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition. Soundness guarantees that the equivalence has enough discriminatory power, completeness ensures that it is maximally permissive. The logical relation is then put to test on the example of noninterference.

awards:
Distinguished Paper
EATCS Best Paper


title: Code Generation via Meta-programming in Dependently Typed Proof Assistants

authors:
Mathis Bouverot-Dupuis
Yannick Forster

abstract: Abstract Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running example: deriving instances for the typeclass. This example is fairly simple, but realistic enough to highlight recurring difficulties with meta-programming: conceptual limitations of frameworks such as term representation – and in particular binder representation –, meta-language expressiveness, and verifiability, as well as current limitations such as API completeness, learning curve, and prover state management, which could in principle be remedied. We conclude with insights regarding features an ideal meta-programming framework should provide.


title: Linear Effects, Exceptions, and Resource Safety - A Curry-Howard Correspondence for Destructors

authors:
Sidney Congard
Guillaume Munch-Maccagnoni
Rémi Douence

abstract: Abstract We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad $$T(- \oplus E)$$ T ( - ⊕ E ) in a linear setting. We consider in particular for T the allocation monad , which we introduce to model and study resource-safety properties. We apply these results to a series of two linear effectful calculi for which we establish their resource-safety properties. The first calculus is a linear (optionally ordered) call-by-push-value language with two allocation effects $${{\,\mathrm{\textbf{new}}\,}}$$ new and $${{\,\mathrm{\textbf{delete}}\,}}$$ delete . The resource-safety properties follow from the linear and ordered character of the typing rules. We then integrate exceptions with linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects $$\delta : A\rightarrow TI$$ δ : A → T I in the slice category over TI . This construction gives rise to a second calculus, the resource call-by-push-value , featuring exceptions and destructors, and whose weakening and exchange rules perform side-effects. It is therefore affine at the level of types but ordered at the level of derivations. As in C++ and Rust, a “move” operation—the side-effecting exchange rule—is necessary for releasing resources in random order, as opposed to LIFO order.


title: Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction -

authors:
John Derrick
Chelsea Edmonds
Andrei Popescu
Jamie Wright

abstract: We make the case that the foundation for Rely-Guarantee reasoning can be fruitfully delivered by a coinductive semantics. Using insight from an Isabelle formalization, via a proof analysis we show that the coinductive semantics tends to simplify the proof development; in particular it enables more direct proofs for the soundness of the Rely-Guarantee rules. The comparison between inductive and coinductive proofs also suggests inductive counterparts of coinductive “up-to” enhancements. On the way, we fill a gap in the literature, by showing that three previously defined inductive semantics for Rely-Guarantee are equivalent. Underlying our transformation of an inductive into a coinductive semantics is the notion of inductively approximating a coinductive predicate—which, deployed in the opposite direction (from coinduction to induction), is a standard technical tool for approximating process algebra bisimilarities. On the spectrum between the abstract fixpoint theorems and concrete instances, we formalize effective format-based criteria that enable sound approximation.


title: Reduction for Structured Concurrent Programs

authors:
Namratha Gangamreddypalli
Constantin Enea
Shaz Qadeer

abstract: Commutativity reasoning based on Lipton’s movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a subset of the initial set of interleavings, which is sound modulo reorderings of commutative actions. Scaling commutativity reasoning to routinely-used features in software systems, such as procedures and parallel composition, remains a significant challenge. In this work, we introduce a novel reduction technique for structured concurrent programs that unifies two key advances. First, we present a reduction strategy that soundly replaces parallel composition with sequential composition. Second, we generalize Lipton’s reduction to support atomic sections containing (potentially recursive) procedure calls. Crucially, these two foundational strategies can be composed arbitrarily, greatly expanding the scope and flexibility of reduction-based reasoning. We implemented this technique in Civl and demonstrated its effectiveness on a number of challenging case studies, including a snapshot object, a fault-tolerant and linearizable register, the FLASH cache coherence protocol, and a non-trivial variant of Two-Phase Commit.


title: Specification-Driven Generation of Summaries for Symbolic Execution

authors:
Rafael Gonçalves
Frederico Ramos
Pedro Adão
José Fragoso Santos

abstract: Abstract Symbolic execution is a popular program analysis technique that has been successfully used for bug-finding and bounded verification in various modern programming languages. Despite its popularity, however, symbolic execution suffers from two main limitations when applied to real-world code: interactions with the runtime environment and path explosion. Symbolic summaries are the standard solution to tackle these challenges. Yet, the development of summaries remains to this day a manual task that is known to be highly error-prone. To address this, we propose SumGen , a new tool for automatically generating correct-by-construction summaries from function specifications. With SumGen , we were able to generate a total of 131 summaries for 47 libc functions, demonstrating the effectiveness of our methodology in producing correct summaries for real-world, highly complex code.