title: On Hierarchical Communication Topologies in the \pi -calculus

authors:
Emanuele D'Osualdo
C.-H. Luke Ong

abstract: This paper is concerned with the shape invariants satisfied by the communication topology of {\pi}-terms, and the automatic inference of these invariants. A {\pi}-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T-shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of {\pi}-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the {\pi}-calculus with decidable safety verification problems.


venue: esop

title: Call-By-Push-Value from a Linear Logic Point of View


title: Visible Type Application

authors:
Richard A. Eisenberg
Stephanie Weirich
Hamidhasan G. Ahmed


title: Automatically Splitting a Two-Stage Lambda Calculus

authors:
Nicolas Feltman
Carlo Angiuli
Umut A. Acar
Kayvon Fatahalian


title: Probabilistic NetKAT

authors:
Nate Foster
Dexter Kozen
Konstantinos Mamouras
Mark Reitblatt
Alexandra Silva


title: Coordinated Concurrent Programming in Syndicate

authors:
Tony Garnock-Jones
Matthias Felleisen


title: An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages

authors:
Daniel Huang
Greg Morrisett


title: Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs

authors:
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Christoph Matheja
Federico Olmedo

abstract: This paper presents a wp---style calculus for obtaining bounds on the expected run---time of probabilistic programs. Its application includes determining the possibly infinite expected termination time of a probabilistic program and proving positive almost---sure termination--does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run---time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson's approach for reasoning about the run---time of deterministic programs. We analyze the expected run---time of some example programs including a one---dimensional random walk and the coupon collector problem.


title: Improving Floating-Point Numbers: A Lazy Approach to Adaptive Accuracy Refinement for Numerical Computations

authors:
Hideyuki Kawabata
Hideya Iwasaki


title: Needle & Knot: Binder Boilerplate Tied Up

authors:
Steven Keuchel
Stephanie Weirich
Tom Schrijvers


title: On the Relative Expressiveness of Higher-Order Session Processes

authors:
Dimitrios Kouzapas
Jorge A. Pérez
Nobuko Yoshida


title: A Classical Realizability Model for a Semantical Value Restriction

abstract: We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).


title: Probabilistic Functions and Cryptographic Oracles in Higher Order Logic


title: Simulating Cities: A Software Engineering Perspective


title: Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

authors:
Cláudio Belo Lourenço
Maria João Frade
Jorge Sousa Pinto


title: Extensible and Efficient Automation Through Reflective Tactics

authors:
Gregory Malecha
Jesper Bengtson


title: An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs

authors:
Antoine Miné
Jason Breck
Thomas W. Reps


title: Functional Big-Step Semantics

authors:
Scott Owens
Magnus O. Myreen
Ramana Kumar
Yong Kiam Tan


title: Classical By-Need

authors:
Pierre-Marie Pédrot
Alexis Saurin


title: Modular Termination Verification for Non-blocking Concurrency

authors:
Pedro da Rocha Pinto
Thomas Dinsdale-Young
Philippa Gardner
Julian Sutherland


title: The Expressive Power of Monotonic Parallel Composition

authors:
Johannes Åman Pohjola
Joachim Parrow


title: Macrofication: Refactoring by Reverse Macro Expansion

authors:
Christopher Schuster
Tim Disney
Cormac Flanagan


title: Type Error Diagnosis for Embedded DSLs by Two-Stage Specialized Type Rules

authors:
Alejandro Serrano
Jurriaan Hage


title: Actor Services - Modular Verification of Message Passing Programs

authors:
Alexander J. Summers
Peter Müller


title: Transfinite Step-Indexing: Decoupling Concrete and Logical Steps

authors:
Kasper Svendsen
Filip Sieczkowski
Lars Birkedal


title: A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

authors:
Yuting Wang
Gopalan Nadathur

abstract: We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language $$\lambda $$λProlog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations that analyze binding structure. We do this by describing concise encodings in $$\lambda $$λProlog for transformations like typed closure conversion and code hoisting that are sensitive to such structure and by showing how to prove their correctness using Abella.


title: Programs Using Syntax with First-Class Binders

authors:
Francisco Ferreira
Brigitte Pientka


title: Disjoint Polymorphism

authors:
João Alpuim
Bruno C. d. S. Oliveira
Zhiyuan Shi


title: Generalizing Inference Systems by Coaxioms

authors:
Davide Ancona
Francesco Dagnino
Elena Zucca

abstract: After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inference rules with the usual meaning, a generalized inference system allows coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proof tree. This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, while providing more flexibility. Indeed, the classical results can be extended to our generalized framework, interpreting recursive definitions as fixed points which are not necessarily the least, nor the greatest one. This allows formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, or are mixed together.


title: Observed Communication Semantics for Classical Processes


title: Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants

authors:
Jasmin Christian Blanchette
Aymeric Bouzy
Andreas Lochbihler
Andrei Popescu
Dmitriy Traytel


title: Confluence of Graph Rewriting with Interfaces

authors:
Filippo Bonchi
Fabio Gadducci
Aleks Kissinger
Pawel Sobocinski
Fabio Zanasi


title: Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency

authors:
Ahmed Bouajjani
Michael Emmi
Constantin Enea
Burcu Kulahcioglu Ozkan
Serdar Tasiran


title: Incremental Update for Graph Rewriting

authors:
Pierre Boutillier
Thomas Ehrhard
Jean Krivine

abstract: International audience


title: Linearity, Control Effects, and Behavioral Types

authors:
Luís Caires
Jorge A. Pérez


title: Temporary Read-Only Permissions for Separation Logic

authors:
Arthur Charguéraud
François Pottier


title: Faster Algorithms for Weighted Recursive State Machines

authors:
Krishnendu Chatterjee
Bernhard Kragl
Samarth Mishra
Andreas Pavlogiannis

abstract: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems.


title: ML and Extended Branching VASS

authors:
Conrad Cotton-Barratt
Andrzej S. Murawski
C.-H. Luke Ong


title: Metric Reasoning About \lambda -Terms: The General Case

authors:
Raphaëlle Crubillé
Ugo Dal Lago


title: Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring

authors:
Ryan Culpepper
Andrew Cobb


title: Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs

authors:
Pedro R. D'Argenio
Gilles Barthe
Sebastian Biewer
Bernd Finkbeiner
Holger Hermanns

abstract:
Usually, it is the software manufacturer who employs verification or testing to ensure that the software embedded in a device meets its main objectives. However, these days we are confronted with the situation that economical or technological reasons might make a manufacturer become interested in the software slightly deviating from its main objective for dubious reasons. Examples include lock-in strategies and the $$\mathrm {NO}_x$$ emission scandals in automotive industry. This phenomenon is what we call software doping. It is turning more widespread as software is embedded in ever more devices of daily use.

The primary contribution of this article is to provide a hierarchy of simple but solid formal definitions that enable to distinguish whether a program is clean or doped. Moreover, we show that these characterisations provide an immediate framework for analysis by using already existing verification techniques. We exemplify this by applying self-composition on sequential programs and model checking of HyperLTL formulas on reactive models.


title: Caper - Automatic Verification for Fine-Grained Concurrency

authors:
Thomas Dinsdale-Young
Pedro da Rocha Pinto
Kristoffer Just Andersen
Lars Birkedal

abstract: Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.


title: Tackling Real-Life Relaxed Concurrency with FSL++

authors:
Marko Doko
Viktor Vafeiadis


title: Extensible Datasort Refinements

abstract: Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes.


title: LINCX: A Linear Logical Framework with First-Class Contexts

authors:
Aïna Linn Georges
Agata Murawska
Shawn Otis
Brigitte Pientka


title: APLicative Programming with Naperian Functors


title: Verified Characteristic Formulae for CakeML

authors:
Armaël Guéneau
Magnus O. Myreen
Ramana Kumar
Michael Norrish

abstract: Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fully-fledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover.


title: Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

authors:
Christina Jansen
Jens Katelaan
Christoph Matheja
Thomas Noll
Florian Zuleger

abstract: We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Previously, such properties have appeared in many places in the separation logic literature, but have not been studied in a systematic manner. In this paper, we develop an algorithmic framework based on heap automata that allows us to derive asymptotically optimal decision procedures for a wide range of robustness properties in a uniform way.


title: Proving Linearizability Using Partial Orders

authors:
Artem Khyzha
Mike Dodds
Alexey Gotsman
Matthew J. Parkinson

abstract:
Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization --- a linear order on operations satisfying the data structure's sequential specification. Proving linearizability is often challenging because an operation's position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof.
We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.


title: The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming

authors:
Cynthia Kop
Jakob Grue Simonsen

abstract:
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice. Cons-freeness roughly means that data constructors cannot occur in function bodies and all manipulation of storage space thus has to happen indirectly using the call stack.

While cons-free programs have previously been used by several authors to characterise complexity classes, the work on non-deterministic programs has almost exclusively considered programs of data order 0. Previous work has shown that adding explicit non-determinism to cons-free programs taking data of order 0 does not increase expressivity; we prove that this--dramatically--is not the case for higher data orders: adding non-determinism to programs with data order at least 1 allows for a characterisation of the entire class of elementary-time decidablei¾?sets.

Finally we show how, even with non-deterministic choice, the original hierarchy of characterisations is restored by imposing different restrictions.


title: The Essence of Higher-Order Concurrent Separation Logic

authors:
Robbert Krebbers
Ralf Jung
Ales Bizjak
Jacques-Henri Jourdan
Derek Dreyer
Lars Birkedal

abstract: Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) and invariants. However, the realization of these concepts in Iris still bakes in several complex mechanisms—such as weakest preconditions and mask-changing view shifts—as primitive notions. In this paper, we take the Iris story to its (so to speak) logical conclusion, applying the reductionist methodology of Iris to Iris itself. Specifically, we define a small, resourceful base logic , which distills the essence of Iris: it comprises only the assertion layer of vanilla separation logic, plus a handful of simple modalities. We then show how the much fancier logical mechanisms of Iris—in particular, its entire program specification layer—can be understood as merely derived forms in our base logic. This approach helps to explain the meaning of Iris’s program specifications at a much higher level of abstraction than was previously possible. We also show that the step-indexed “later” modality of Iris is an essential source of complexity, in that removing it leads to a logical inconsistency. All our results are fully formalized in the Coq proof assistant.


title: Comprehending Isabelle/HOL's Consistency

authors:
Ondrej Kuncar
Andrei Popescu

abstract: The proof assistant Isabelle/HOL is based on an extension of Higher-Order Logic HOL with ad hoc overloading of constants. It turns out that the interaction between the standard HOL type definitions and the Isabelle-specific ad hoc overloading is problematic for the logical consistency. In previous work, we have argued that standard HOL semantics is no longer appropriate for capturing this interaction, and have proved consistency using a nonstandard semantics. The use of an exotic semantics makes that proof hard to digest by the community. In this paper, we prove consistency by proof-theoretic means--following the healthy intuition of definitions as abbreviations, realized in HOLC, a logic that augments HOL with comprehension types. We hope that our new proof settles the Isabelle/HOL consistency problem once and for all. In addition, HOLC offers a framework for justifying the consistency of new deduction schemas that address practical user needs.


title: Probabilistic Termination by Monadic Affine Sized Typing

authors:
Ugo Dal Lago
Charles Grellois

abstract: We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.


title: The Essence of Functional Programming on Semantic Data

authors:
Martin Leinberger
Ralf Lämmel
Steffen Staab


title: A Classical Sequent Calculus with Dependent Types


title: Context-Free Session Type Inference


title: Modular Verification of Higher-Order Functional Programs

authors:
Ryosuke Sato
Naoki Kobayashi


title: Commutative Semantics for Probabilistic Programming


title: Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization

authors:
Hao Tang
Di Wang
Yingfei Xiong
Lingming Zhang
Xiaoyin Wang
Lu Zhang


title: A Higher-Order Logic for Concurrent Termination-Preserving Refinement

authors:
Joseph Tassarotti
Ralf Jung
Robert Harper

abstract: Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.


title: Modular Verification of Procedure Equivalence in the Presence of Memory Allocation

authors:
Tim Wood
Sophia Drossopoulou
Shuvendu K. Lahiri
Susan Eisenbach


title: Abstract Specifications for Concurrent Maps

authors:
Shale Xiong
Pedro da Rocha Pinto
Gian Ntzik
Philippa Gardner


title: Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

authors:
Alejandro Aguirre
Gilles Barthe
Lars Birkedal
Ales Bizjak
Marco Gaboardi
Deepak Garg

abstract: We extend the simply-typed guarded $$\lambda $$ -calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types. The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.


title: Higher-Order Program Verification via HFL Model Checking

authors:
Naoki Kobayashi
Takeshi Tsukada
Keiichi Watanabe

abstract: There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have not been well studied. In the present paper, we show that various verification problems for functional programs, including may/must-reachability, trace properties, and linear-time temporal properties (and their negations), can be naturally reduced to (extended) HFL model checking. The reductions yield a sound and complete logical characterization of those program properties. Compared with the previous approaches based on HORS model checking, our approach provides a more uniform, streamlined method for higher-order program verification.


title: Fragment Abstraction for Concurrent Shape Analysis

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Cong Quy Trinh

abstract: A major challenge in automated verification is to develop techniques that are able to reason about fine-grained concurrent algorithms that consist of an unbounded number of concurrent threads, which operate on an unbounded domain of data values, and use unbounded dynamically allocated memory. Existing automated techniques consider the case where shared data is organized into singly-linked lists. We present a novel shape analysis for automated verification of fine-grained concurrent algorithms that can handle heap structures which are more complex than just singly-linked lists, in particular skip lists and arrays of singly linked lists, while at the same time handling an unbounded number of concurrent threads, an unbounded domain of data values (including timestamps), and an unbounded shared heap. Our technique is based on a novel shape abstraction, which represents a set of heaps by a set of fragments . A fragment is an abstraction of a pair of heap cells that are connected by a pointer field. We have implemented our approach and applied it to automatically verify correctness, in the sense of linearizability, of most linearizable concurrent implementations of sets, stacks, and queues, which employ singly-linked lists, skip lists, or arrays of singly-linked lists with timestamps, which are known to us in the literature.


title: Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach

authors:
Joaquín Aguado
Michael Mendler
Marc Pouzet
Partha S. Roop
Reinhard von Hanxleden

abstract: Synchronous Programming ( SP ) is a universal computational principle that provides deterministic concurrency. The same input sequence with the same timing always results in the same externally observable output sequence, even if the internal behaviour generates uncertainty in the scheduling of concurrent memory accesses. Consequently, SP languages have always been strongly founded on mathematical semantics that support formal program analysis. So far, however, communication has been constrained to a set of primitive clock-synchronised shared memory ( csm ) data types, such as data-flow registers, streams and signals with restricted read and write accesses that limit modularity and behavioural abstractions. This paper proposes an extension to the SP theory which retains the advantages of deterministic concurrency, but allows communication to occur at higher levels of abstraction than currently supported by SP data types. Our approach is as follows. To avoid data races, each csm type publishes a policy interface for specifying the admissibility and precedence of its access methods. Each instance of the csm type has to be policy-coherent, meaning it must behave deterministically under its own policy—a natural requirement if the goal is to build deterministic systems that use these types. In a policy-constructive system, all access methods can be scheduled in a policy-conformant way for all the types without deadlocking. In this paper, we show that a policy-constructive program exhibits deterministic concurrency in the sense that all policy-conformant interleavings produce the same input-output behaviour. Policies are conservative and support the csm types existing in current SP languages. Technically, we introduce a kernel SP language that uses arbitrary policy-driven csm types. A big-step fixed-point semantics for this language is developed for which we prove determinism and termination of constructive programs.


title: An Assertion-Based Program Logic for Probabilistic Programs

authors:
Gilles Barthe
Thomas Espitau
Marco Gaboardi
Benjamin Grégoire
Justin Hsu
Pierre-Yves Strub

abstract: We present Ellora , a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora . These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times

authors:
Kevin Batz
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Christoph Matheja

abstract: Bayesian networks (BNs) are probabilistic graphical models for describing complex joint probability distributions. The main problem for BNs is inference: Determine the probability of an event given observed evidence. Since exact inference is often infeasible for large BNs, popular approximate inference methods rely on sampling. We study the problem of determining the expected time to obtain a single valid sample from a BN. To this end, we translate the BN together with observations into a probabilistic program. We provide proof rules that yield the exact expected runtime of this program in a fully automated fashion. We implemented our approach and successfully analyzed various real–world BNs taken from the Bayesian network repository.


title: Fine-Grained Semantics for Probabilistic Programs

authors:
Benjamin Bichsel
Timon Gehr
Martin T. Vechev

abstract: Probabilistic programming is an emerging technique for modeling processes involving uncertainty. Thus, it is important to ensure these programs are assigned precise formal semantics that also cleanly handle typical exceptions such as non-termination or division by zero. However, existing semantics of probabilistic programs do not fully accommodate different exceptions and their interaction, often ignoring some or conflating multiple ones into a single exception state, making it impossible to distinguish exceptions or to study their interaction. In this paper, we provide an expressive probabilistic programming language together with a fine-grained measure-theoretic denotational semantics that handles and distinguishes non-termination, observation failures and error states. We then investigate the properties of this semantics, focusing on the interaction of different kinds of exceptions. Our work helps to better understand the intricacies of probabilistic programs and ensures their behavior matches the intended semantics.


title: Quantitative Analysis of Smart Contracts

authors:
Krishnendu Chatterjee
Amir Kafshdar Goharshady
Yaron Velner

abstract: Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i) a simplified programming language for smart contracts; (ii) an automatic translation of the programs to state-based games; (iii) an abstraction-refinement approach to solve such games; and (iv) experimental results on real-world-inspired smart contracts.


title: Compositional Verification of Compiler Optimisations on Relaxed Memory

authors:
Mike Dodds
Mark Batty
Alexey Gotsman

abstract: A valid compiler optimisation transforms a block in a program without introducing new observable behaviours to the program as a whole. Deciding which optimisations are valid can be difficult, and depends closely on the semantic model of the programming language. Axiomatic relaxed models, such as C++11, present particular challenges for determining validity, because such models allow subtle effects of a block transformation to be observed by the rest of the program. In this paper we present a denotational theory that captures optimisation validity on an axiomatic model corresponding to a fragment of C++11. Our theory allows verifying an optimisation compositionally, by considering only the block it transforms instead of the whole program. Using this property, we realise the theory in the first push-button tool that can verify real-world optimisations under an axiomatic memory model.


title: Modular Product Programs

authors:
Marco Eilers
Peter Müller
Samuel Hitz

abstract: Many interesting program properties like determinism or information flow security are hyperproperties, that is, they relate multiple executions of the same program. Hyperproperties can be verified using relational logics, but these logics require dedicated tool support and are difficult to automate. Alternatively, constructions such as self-composition represent multiple executions of a program by one product program, thereby reducing hyperproperties of the original program to trace properties of the product. However, existing constructions do not fully support procedure specifications, for instance, to derive the determinism of a caller from the determinism of a callee, making verification non-modular. We present modular product programs, a novel kind of product program that permits hyperproperties in procedure specifications and, thus, can reason about calls modularly. We demonstrate its expressiveness by applying it to information flow security with advanced features such as declassification and termination-sensitivity. Modular product programs can be verified using off-the-shelf verifiers; we have implemented our approach to secure information flow using the Viper verification infrastructure.


title: Correctness of a Concurrent Object Collector for Actor Languages

authors:
Juliana Franco
Sylvan Clebsch
Sophia Drossopoulou
Jan Vitek
Tobias Wrigstad

abstract: ORCA is a garbage collection protocol for actor-based programs. Multiple actors may mutate the heap while the collector is running without any dedicated synchronisation. ORCA is applicable to any actor language whose type system prevents data races and which supports causal message delivery. We present a model of ORCA which is parametric to the host language and its type system. We describe the interplay between the host language and the collector. We give invariants preserved by ORCA , and prove its soundness and completeness.


title: Paxos Consensus, Deconstructed and Abstracted

authors:
Álvaro García-Pérez
Alexey Gotsman
Yuri Meshman
Ilya Sergey

abstract: Lamport’s Paxos algorithm is a classic consensus protocol for state machine replication in environments that admit crash failures. Many versions of Paxos exploit the protocol’s intrinsic properties for the sake of gaining better run-time performance, thus widening the gap between the original description of the algorithm, which was proven correct, and its real-world implementations. In this work, we address the challenge of specifying and verifying complex Paxos-based systems by (a) devising composable specifications for implementations of Paxos’s single-decree version, and (b) engineering disciplines to reason about protocol-aware, semantics-preserving optimisations to single-decree Paxos. In a nutshell, our approach elaborates on the deconstruction of single-decree Paxos by Boichat et al. We provide novel non-deterministic specifications for each module in the deconstruction and prove that the implementations refine the corresponding specifications, such that the proofs of the modules that remain unchanged can be reused across different implementations. We further reuse this result and show how to obtain a verified implementation of Multi-Paxos from a verified implementation of single-decree Paxos, by a series of novel protocol-aware transformations of the network semantics, which we prove to be behaviour-preserving. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Session-Typed Concurrent Contracts

authors:
Hannah Gommerstadt
Limin Jia
Frank Pfenning

abstract: In sequential languages, dynamic contracts are usually expressed as boolean functions without externally observable effects, written within the language. We propose an analogous notion of concurrent contracts for languages with session-typed message-passing concurrency. Concurrent contracts are partial identity processes that monitor the bidirectional communication along channels and raise an alarm if a contract is violated. Concurrent contracts are session-typed in the usual way and must also satisfy a transparency requirement, which guarantees that terminating compliant programs with and without the contracts are observationally equivalent. We illustrate concurrent contracts with several examples. We also show how to generate contracts from a refinement session-type system and show that the resulting monitors are redundant for programs that are well-typed.


title: A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

authors:
Armaël Guéneau
Arthur Charguéraud
François Pottier

abstract: We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.


title: Deadlock-Free Monitors

authors:
Jafar Hamin
Bart Jacobs

abstract: Monitors constitute one of the common techniques to synchronize threads in multithreaded programs, where calling a $$\mathsf {wait}$$ command on a condition variable suspends the caller thread and notifying a condition variable causes the threads waiting for that condition variable to resume their execution. One potential problem with these programs is that a waiting thread might be suspended forever leading to deadlock, a state where each thread of the program is waiting for a condition variable or a lock. In this paper, a modular verification approach for deadlock-freedom of such programs is presented, ensuring that in any state of the execution of the program if there are some threads suspended then there exists at least one thread running. The main idea behind this approach is to make sure that for any condition variable v for which a thread is waiting there exists a thread obliged to fulfil an obligation for v that only waits for a waitable object whose wait level, an arbitrary number associated with each waitable object, is less than the wait level of v. The relaxed precedence relation introduced in this paper, aiming to avoid cycles, can also benefit some other verification approaches, verifying deadlock-freedom of other synchronization constructs such as channels and semaphores, enabling them to accept a wider range of deadlock-free programs. We encoded the proposed proof rules in the VeriFast program verifier and by defining some appropriate invariants for the locks associated with some condition variables succeeded in verifying some popular use cases of monitors including unbounded/bounded buffer, sleeping barber, barrier, and readers-writers locks. A soundness proof for the presented approach is provided; some of the trickiest lemmas in this proof have been machine-checked with Coq.


title: A Verified Compiler from Isabelle/HOL to CakeML

authors:
Lars Hupel
Tobias Nipkow

abstract: Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.


title: Eventual Consistency for CRDTs

authors:
Radha Jagadeesan
James Riely

abstract: We address the problem of validity in eventually consistent (EC) systems: In what sense does an EC data structure satisfy the sequential specification of that data structure? Because EC is a very weak criterion, our definition does not describe every EC system; however it is expressive enough to describe any Convergent or Commutative Replicated Data Type (CRDT).


title: Concurrent Kleene Algebra: Free Model and Completeness

authors:
Tobias Kappé
Paul Brunet
Alexandra Silva
Fabio Zanasi

abstract: Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with bounded parallelism are complete for the semantics proposed in the original paper; consequently, these semantics are the free model for this fragment. This result settles a conjecture of Hoare and collaborators. Moreover, the technique developed to this end allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.


title: Logical Reasoning for Disjoint Permissions

authors:
Xuan Bach Le
Aquinas Hobor

abstract: Resource sharing is a fundamental phenomenon in concurrent programming where several threads have permissions to access a common resource. Logics for verification need to capture the notion of permission ownership and transfer. One typical practice is the use of rational numbers in (0, 1] as permissions in which 1 is the full permission and the rest are fractional permissions. Rational permissions are not a good fit for separation logic because they remove the essential “disjointness” feature of the logic itself. We propose a general logic framework that supports permission reasoning in separation logic while preserving disjointness. Our framework is applicable to sophisticated verification tasks such as doing induction over the finiteness of the heap within the object logic or carrying out biabductive inference. We can also prove precision of recursive predicates within the object logic. We developed the ShareInfer tool to benchmark our techniques. We introduce “scaling separation algebras,” a compositional extension of separation algebras, to model our logic, and use them to construct a concrete model.


title: HOBiT: Programming Lenses Without Using Lens Combinators

authors:
Kazutaka Matsuda
Meng Wang

abstract: We propose HOBiT, a higher-order bidirectional programming language, in which users can write bidirectional programs in the familiar style of conventional functional programming, while enjoying the full expressiveness of lenses. A bidirectional transformation, or a lens, is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws—a pattern that is found in databases, model-driven development, compiler construction, and so on. The most common way of programming lenses is with lens combinators, which are lens-to-lens functions that compose simpler lenses to form more complex ones. Lens combinators preserve the bidirectionality of lenses and are expressive; but they compel programmers to a specialised point-free style—i.e., no naming of intermediate computation results—limiting the scalability of bidirectional programming. To address this issue, we propose a new bidirectional programming language HOBiT, in which lenses are represented as standard functions, and combinators are mapped to language constructs with binders. This design transforms bidirectional programming, enabling programmers to write bidirectional programs in a flexible functional style and at the same time access the full expressiveness of lenses. We formally define the syntax, type system, and the semantics of the language, and then show that programs in HOBiT satisfy bidirectionality. Additionally, we demonstrate HOBiT ’s programmability with examples.


title: Verified Learning Without Regret - From Algorithmic Game Theory to Distributed Systems with Mechanized Complexity Guarantees

authors:
Samuel Merten
Alexander Bagnall
Gordon Stewart

abstract: Multiplicative Weights (MW) is a simple yet powerful algorithm for learning linear classifiers, for ensemble learning à la boosting, for approximately solving linear and semidefinite systems, for computing approximate solutions to multicommodity flow problems, and for online convex optimization, among other applications. Recent work in algorithmic game theory, which applies a computational perspective to the design and analysis of systems with mutually competitive actors, has shown that no-regret algorithms like MW naturally drive games toward approximate Coarse Correlated Equilibria (CCEs), and that for certain games, approximate CCEs have bounded cost with respect to the optimal states of such systems. In this paper, we put such results to practice by building distributed systems such as routers and load balancers with performance and convergence guarantees mechanically verified in Coq. The main contributions on which our results rest are (1) the first mechanically verified implementation of Multiplicative Weights (specifically, we show that our MW is no regret) and (2) a language-based formulation, in the form of a DSL, of the class of games satisfying Roughgarden smoothness, a broad characterization of those games whose approximate CCEs have cost bounded with respect to optimal. Composing (1) with (2) within Coq yields a new strategy for building distributed systems with mechanically verified complexity guarantees on the time to convergence to near-optimal system configurations.


title: Program Verification by Coinduction

authors:
Brandon M. Moore
Lucas Peña
Grigore Rosu

abstract: We present a novel program verification approach based on coinduction, which takes as input an operational semantics. No intermediates like program logics or verification condition generators are needed. Specifications can be written using any state predicates. We implement our approach in Coq, giving a certifying language-independent verification framework. Our proof system is implemented as a single module imported unchanged into language-specific proofs. Automation is reached by instantiating a generic heuristic with language-specific tactics. Manual assistance is also smoothly allowed at points the automation cannot handle. We demonstrate the power and versatility of our approach by verifying algorithms as complicated as Schorr-Waite graph marking and instantiating our framework for object languages in several styles of semantics. Finally, we show that our coinductive approach subsumes reachability logic, a recent language-independent sound and (relatively) complete logic for program verification that has been instantiated with operational semantics of languages as complex as C, Java and JavaScript. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Dualizing Generalized Algebraic Data Types by Matrix Transposition

authors:
Klaus Ostermann
Julian Jabs

abstract: We characterize the relation between generalized algebraic datatypes (GADTs) with pattern matching on their constructors one hand, and generalized algebraic co-datatypes (GAcoDTs) with copattern matching on their destructors on the other hand: GADTs can be converted mechanically to GAcoDTs by refunctionalization, GAcoDTs can be converted mechanically to GADTs by defunctionalization, and both defunctionalization and refunctionalization correspond to a transposition of the matrix in which the equations for each constructor/destructor pair of the (co-)datatype are organized. We have defined a calculus, $$GADT^T$$ , which unifies GADTs and GAcoDTs in such a way that GADTs and GAcoDTs are merely different ways to partition the program. We have formalized the type system and operational semantics of $$GADT^T$$ in the Coq proof assistant and have mechanically verified the following results: (1) The type system of $$GADT^T$$ is sound, (2) defunctionalization and refunctionalization can translate GADTs to GAcoDTs and back, (3) both transformations are type- and semantics-preserving and are inverses of each other, (4) (co-)datatypes can be represented by matrices in such a way the aforementioned transformations correspond to matrix transposition, (5) GADTs are extensible in an exactly dual way to GAcoDTs; we thereby clarify folklore knowledge about the “expression problem”. We believe that the identification of this relationship can guide future language design of “dual features” for data and codata.


title: Failure is Not an Option - An Exceptional Type Theory

authors:
Pierre-Marie Pédrot
Nicolas Tabareau

abstract: We define the exceptional translation, a syntactic translation of the Calculus of Inductive Constructions (CIC) into itself, that covers full dependent elimination. The new resulting type theory features call-by-name exceptions with decidable type-checking and canonicity, but at the price of inconsistency. Then, noticing parametricity amounts to Kreisel’s realizability in this setting, we provide an additional layer on top of the exceptional translation in order to tame exceptions and ensure that all exceptions used locally are caught, leading to the parametric exceptional translation which fully preserves consistency. This way, we can consistently extend the logical expressivity of CIC with independence of premises, Markov’s rule, and the negation of function extensionality while retaining $$\eta $$ -expansion. As a byproduct, we also show that Markov’s principle is not provable in CIC. Both translations have been implemented in a Coq plugin, which we use to formalize the examples.


title: On Parallel Snapshot Isolation and Release/Acquire Consistency

authors:
Azalea Raad
Ori Lahav
Viktor Vafeiadis

abstract: Parallel snapshot isolation (PSI) is a standard transactional consistency model used in databases and distributed systems. We argue that PSI is also a useful formal model for software transactional memory (STM) as it has certain advantages over other consistency models. However, the formal PSI definition is given declaratively by acyclicity axioms, which most programmers find hard to understand and reason about. To address this, we develop a simple lock-based reference implementation for PSI built on top of the release-acquire memory model, a well-behaved subset of the C/C++11 memory model. We prove that our implementation is sound and complete against its higher-level declarative specification. We further consider an extension of PSI allowing transactional and non-transactional code to interact, and provide a sound and complete reference implementation for the more general setting. Supporting this interaction is necessary for adopting a transactional model in programming languages. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq

authors:
Vincent Rahli
Ivana Vukotic
Marcus Völp
Paulo Jorge Esteves Veríssimo

abstract: Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least $$n-f$$ out of n replicas survive arbitrary faults. This paper presents Velisarios, a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT.


title: Explicit Effect Subtyping

authors:
Amr Hany Saleh
Georgios Karachalias
Matija Pretnar
Tom Schrijvers

abstract: As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly error-prone because its core language is implicitly-typed, making code transformations very fragile. To remedy this, we present an explicitly-typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly-typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content.


title: Behavioural Equivalence via Modalities for Algebraic Effects

authors:
Alex Simpson
Niels F. W. Voorneveld

abstract: The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.


title: Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management

authors:
Lau Skorstengaard
Dominique Devriese
Lars Birkedal

abstract: Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: A Separation Logic for a Promising Semantics

authors:
Kasper Svendsen
Jean Pichon-Pharabod
Marko Doko
Ori Lahav
Viktor Vafeiadis

abstract: We present SLR, the first expressive program logic for reasoning about concurrent programs under a weak memory model addressing the out-of-thin-air problem. Our logic includes the standard features from existing logics, such as RSL and GPS, that were previously known to be sound only under stronger memory models: (1) separation, (2) per-location invariants, and (3) ownership transfer via release-acquire synchronisation—as well as novel features for reasoning about (4) the absence of out-of-thin-air behaviours and (5) coherence. The logic is proved sound over the recent “promising” memory model of Kang et al., using a substantially different argument to soundness proofs of logics for simpler memory models.


title: On Polymorphic Sessions and Functions - A Tale of Two (Fully Abstract) Encodings

authors:
Bernardo Toninho
Nobuko Yoshida

abstract: This work exploits the logical foundation of session types to determine what kind of type discipline for the $$\pi $$ -calculus can exactly capture, and is captured by, $$\lambda $$ -calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session $$\pi $$ -calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the $$\lambda $$ -calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.


title: An Abstract Interpretation Framework for Input Data Usage

authors:
Caterina Urban
Peter Müller

abstract: Data science software plays an increasingly important role in critical decision making in fields ranging from economy and finance to biology and medicine. As a result, errors in data science applications can have severe consequences, especially when they lead to results that look plausible, but are incorrect. A common cause of such errors is when applications erroneously ignore some of their input data, for instance due to bugs in the code that reads, filters, or clusters it. In this paper, we propose an abstract interpretation framework to automatically detect unused input data. We derive a program semantics that precisely captures data usage by abstraction of the program’s operational trace semantics and express it in a constructive fixpoint form. Based on this semantics, we systematically derive static analyses that automatically detect unused input data by fixpoint approximation. This clear design principle provides a framework that subsumes existing analyses; we show that secure information flow analyses and a form of live variables analysis can be used for data usage, with varying degrees of precision. Additionally, we derive a static analysis to detect single unused data inputs, which is similar to dependency analyses used in the context of backward program slicing. Finally, we demonstrate the value of expressing such analyses as abstract interpretation by combining them with an existing abstraction of compound data structures such as arrays and lists to detect unused chunks of the data. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems

authors:
Malte Viering
Tzu-Chun Chen
Patrick Eugster
Raymond Hu
Lukasz Ziarek

abstract: A key requirement for many distributed systems is to be resilient toward partial failures, allowing a system to progress despite the failure of some components. This makes programming of such systems daunting, particularly in regards to avoiding inconsistencies due to failures and asynchrony. This work introduces a formal model for crash failure handling in asynchronous distributed systems featuring a lightweight coordinator, modeled in the image of widely used systems such as ZooKeeper and Chubby. We develop a typing discipline based on multiparty session types for this model that supports the specification and static verification of multiparty protocols with explicit failure handling. We show that our type system ensures subject reduction and progress in the presence of failures. In other words, in a well-typed system even if some participants crash during execution, the system is guaranteed to progress in a consistent manner with the remaining participants.


title: Evaluating Design Tradeoffs in Numeric Static Analysis for Java

authors:
Shiyi Wei
Piotr Mardziel
Andrew Ruef
Jeffrey S. Foster
Michael Hicks

abstract: Numeric static analysis for Java has a broad range of potentially useful applications, including array bounds checking and resource usage estimation. However, designing a scalable numeric static analysis for real-world Java programs presents a multitude of design choices, each of which may interact with others. For example, an analysis could handle method calls via either a top-down or bottom-up interprocedural analysis. Moreover, this choice could interact with how we choose to represent aliasing in the heap and/or whether we use a relational numeric domain, e.g., convex polyhedra. In this paper, we present a family of abstract interpretation-based numeric static analyses for Java and systematically evaluate the impact of 162 analysis configurations on the DaCapo benchmark suite. Our experiment considered the precision and performance of the analyses for discharging array bounds checks. We found that top-down analysis is generally a better choice than bottom-up analysis, and that using access paths to describe heap objects is better than using summary objects corresponding to points-to analysis locations. Moreover, these two choices are the most significant, while choices about the numeric domain, representation of abstract objects, and context-sensitivity make much less difference to the precision/performance tradeoff.


title: Consistent Subtyping for All

authors:
Ningning Xie
Xuan Bi
Bruno C. d. S. Oliveira

abstract: Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this paper is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping, and subsumes the original definition by Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this paper is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing, which are mechanically formalized using the Coq proof assistant. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Let Arguments Go First

authors:
Ningning Xie
Bruno C. d. S. Oliveira

abstract: Bi-directional type checking has proved to be an extremely useful and versatile tool for type checking and type inference. The conventional presentation of bi-directional type checking consists of two modes: inference mode and checked mode. In traditional bi-directional type-checking, type annotations are used to guide (via the checked mode) the type inference/checking procedure to determine the type of an expression, and type information flows from functions to arguments . This paper presents a variant of bi-directional type checking where the type information flows from arguments to functions . This variant retains the inference mode, but adds a so-called application mode. Such design can remove annotations that basic bi-directional type checking cannot, and is useful when type information from arguments is required to type-check the functions being applied. We present two applications and develop the meta-theory (mostly verified in Coq) of the application mode. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Types by Need

authors:
Beniamino Accattoli
Giulio Guerrieri
Maico Leberle

abstract: A cornerstone of the theory of $$\lambda $$ -calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.


title: Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog

authors:
Mario Alvarez-Picallo
Alex Eyers-Taylor
Michael Peyton Jones
C.-H. Luke Ong

abstract: Incremental computation has recently been studied using the concepts of change structures and derivatives of programs, where the derivative of a function allows updating the output of the function based on a change to its input. We generalise change structures to change actions , and study their algebraic properties. We develop change actions for common structures in computer science, including directed-complete partial orders and Boolean algebras. We then show how to compute derivatives of fixpoints. This allows us to perform incremental evaluation and maintenance of recursively defined functions with particular application generalised Datalog programs. Moreover, unlike previous results, our techniques are modular in that they are easy to apply both to variants of Datalog and to other programming languages.


title: Manifest Deadlock-Freedom for Shared Session Types

authors:
Stephanie Balzer
Bernardo Toninho
Frank Pfenning

abstract: Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed $$\pi $$ -calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a locking discipline of acquire-release. While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems. In this paper, we develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing, and recursive processes. We illustrate our approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.


title: Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

authors:
Henning Basold
Ekaterina Komendantskaya
Yue Li

abstract: We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs ; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.


title: Compiling Sandboxes: Formally Verified Software Fault Isolation

authors:
Frédéric Besson
Sandrine Blazy
Alexandre Dang
Thomas P. Jensen
Pierre Wilke

abstract: Software Fault Isolation (SFI) is a security-enhancing program transformation for instrumenting an untrusted binary module so that it runs inside a dedicated isolated address space, called a sandbox. To ensure that the untrusted module cannot escape its sandbox, existing approaches such as Google’s Native Client rely on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, we design, implement and prove correct a program instrumentation phase as part of the formally verified compiler CompCert that enforces a sandboxing security property a priori . This eliminates the need for a binary verifier and, instead, leverages the soundness proof of the compiler to prove the security of the sandboxing transformation. The technical contributions are a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers, and a formally verified C compiler that implements SFI. Experiments show that our formally verified technique is a competitive way of implementing SFI.


title: Distributive Disjoint Polymorphism for Compositional Programming

authors:
Xuan Bi
Ningning Xie
Bruno C. d. S. Oliveira
Tom Schrijvers

abstract: Popular programming techniques such as shallow embeddings of Domain Specific Languages (DSLs), finally tagless or object algebras are built on the principle of compositionality. However, existing programming languages only support simple compositional designs well, and have limited support for more sophisticated ones. This paper presents the $$\mathsf {F}_{i}^{+}$$ calculus, which supports highly modular and compositional designs that improve on existing techniques. These improvements are due to the combination of three features: disjoint intersection types with a merge operator; parametric (disjoint) polymorphism; and BCD-style distributive subtyping. The main technical challenge is $$\mathsf {F}_{i}^{+}$$ ’s proof of coherence. A naive adaptation of ideas used in System F’s parametricity to canonicity (the logical relation used by $$\mathsf {F}_{i}^{+}$$ to prove coherence) results in an ill-founded logical relation. To solve the problem our canonicity relation employs a different technique based on immediate substitutions and a restriction to predicative instantiations. Besides coherence, we show several other important meta-theoretical results, such as type-safety, sound and complete algorithmic subtyping, and decidability of the type system. Remarkably, unlike $$\mathsf {F}_{<:}$$ ’s bounded polymorphism, disjoint polymorphism in $$\mathsf {F}_{i}^{+}$$ supports decidable type-checking.


title: Asynchronous Timed Session Types - From Duality to Time-Sensitive Processes

authors:
Laura Bocchi
Maurizio Murgia
Vasco Thudichum Vasconcelos
Nobuko Yoshida

abstract: We present a behavioural typing system for a higher-order timed calculus using session types to model timed protocols. Behavioural typing ensures that processes in the calculus perform actions in the time-windows prescribed by their protocols. We introduce duality and subtyping for timed asynchronous session types. Our notion of duality allows typing a larger class of processes with respect to previous proposals. Subtyping is critical for the precision of our typing system, especially in the presence of session delegation. The composition of dual (timed asynchronous) types enjoys progress when using an urgent receive semantics, in which receive actions are executed as soon as the expected message is available. Our calculus increases the modelling power of extant calculi on timed sessions, adding a blocking receive primitive with timeout and a primitive that consumes an arbitrary amount of time in a given range.


title: Counters in Kappa: Semantics, Simulation, and Static Analysis

authors:
Pierre Boutillier
Ioana Cristescu
Jérôme Feret

abstract: Site-graph rewriting languages, such as Kappa or BNGL, offer parsimonious ways to describe highly combinatorial systems of mechanistic interactions among proteins. These systems may be then simulated efficiently. Yet, the modeling mechanisms that involve counting (a number of phosphorylated sites for instance) require an exponential number of rules in Kappa. In BNGL, updating the set of the potential applications of rules in the current state of the system comes down to the sub-graph isomorphism problem (which is NP-complete). In this paper, we extend Kappa to deal both parsimoniously and efficiently with counters. We propose a single push-out semantics for Kappa with counters. We show how to compile Kappa with counters into Kappa without counters (without requiring an exponential number of rules). We design a static analysis, based on affine relationships, to identify the meaning of counters and bound their ranges accordingly.


title: On the Multi-Language Construction

authors:
Samuele Buro
Isabella Mastroeni

abstract: Modern software is no more developed in a single programming language. Instead, programmers tend to exploit cross-language interoperability mechanisms to combine code stemming from different languages, and thus yielding fully-fledged multi-language programs . Whilst this approach enables developers to benefit from the strengths of each single-language, on the other hand it complicates the semantics of such programs. Indeed, the resulting multi-language does not meet any of the semantics of the combined languages. In this paper, we broaden the boundary functions -based approach à la Matthews and Findler to propose an algebraic framework that provides a constructive mathematical notion of multi-language able to determine its semantics . The aim of this work is to overcome the lack of a formal method (resp., model) to design (resp., represent) a multi-language, regardless of the inherent nature of the underlying languages. We show that our construction ensures the uniqueness of the semantic function (i.e., the multi-language semantics induced by the combined languages) by proving the initiality of the term model (i.e., the abstract syntax of the multi-language) in its category.


title: Probabilistic Programming Inference via Intensional Semantics

authors:
Simon Castellan
Hugo Paquet

abstract: We define a new denotational semantics for a first-order probabilistic programming language in terms of probabilistic event structures . This semantics is intensional , meaning that the interpretation of a program contains information about its behaviour throughout execution, rather than a simple distribution on return values. In particular, occurrences of sampling and conditioning are recorded as explicit events, partially ordered according to the data dependencies between the corresponding statements in the program. This interpretation is adequate : we show that the usual measure-theoretic semantics of a program can be recovered from its event structure representation. Moreover it can be leveraged for MCMC inference: we prove correct a version of single-site Metropolis-Hastings with incremental recomputation , in which the proposal kernel takes into account the semantic information in order to avoid performing some of the redundant sampling.


title: Data Races and Static Analysis for Interrupt-Driven Kernels

authors:
Nikita Chopra
Rekha R. Pai
Deepak D'Souza

abstract: We consider a class of interrupt-driven programs that model the kernel API libraries of some popular real-time embedded operating systems and the synchronization mechanisms they use. We define a natural notion of data races and a happens-before ordering for such programs. The key insight is the notion of disjoint blocks to define the synchronizes-with relation. This notion also suggests an efficient and effective lockset based analysis for race detection. It also enables us to define efficient “sync-CFG” based static analyses for such programs, which exploit data race freedom. We use this theory to carry out static analysis on the FreeRTOS kernel library to detect races and to infer simple relational invariants on key kernel variables and data-structures.


title: Codata in Action

authors:
Paul Downen
Zachary Sullivan
Zena M. Ariola
Simon Peyton Jones

abstract: Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language: eager or lazy, statically or dynamically typed, and functional or object-oriented. While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter-compilation techniques between data and codata. We believe codata is a common ground between the functional and object-oriented paradigms; ultimately, we hope to utilize the Curry-Howard isomorphism to further bridge the gap.


title: Semi-automated Reasoning About Non-determinism in C Expressions

authors:
Dan Frumin
Léon Gondelman
Robbert Krebbers

abstract: Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called “sequence point violations”. These aspects should be accounted for in verification because C compilers exploit them. We present a verification condition generator (vcgen) that enables one to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty of our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition . The frame is used to automatically determine how resources should be distributed among subexpressions. We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C . This semantics is modular and gives a concise account of non-determinism in C . We have implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for the new monadic definitional semantics of a subset of C .


title: A Static Higher-Order Dependency Pair Framework

authors:
Carsten Fuhs
Cynthia Kop

abstract: We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA .


title: Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation

authors:
Paolo G. Giarrusso
Yann Régis-Gianas
Philipp Schuster

abstract: Incremental computation requires propagating changes and reusing intermediate results of base computations. Derivatives, as produced by static differentiation [7], propagate changes but do not reuse intermediate results, leading to wasteful recomputation. As a solution, we introduce conversion to Cache-Transfer-Style, an additional program transformations producing purely incremental functional programs that create and maintain nested tuples of intermediate results. To prove CTS conversion correct, we extend the correctness proof of static differentiation from STLC to untyped $$\lambda $$ -calculus via step-indexed logical relations, and prove sound the additional transformation via simulation theorems. To show ILC-based languages can improve performance relative to from-scratch recomputation, and that CTS conversion can extend its applicability, we perform an initial performance case study. We provide derivatives of primitives for operations on collections and incrementalize selected example programs using those primitives, confirming expected asymptotic speedups.


title: Verifiable Certificates for Predicate Subtyping

abstract: Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, with the exception of the definition of conversion, which is based on a specific notion of reduction $$\rightarrow _{\beta *}$$ , corresponding to $$\beta $$ -reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction $$\rightarrow _{\beta \sigma }$$ allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of $$\rightarrow _{\beta \sigma }$$ and strong normalization of both $$\rightarrow _{\beta \sigma }$$ and $$\rightarrow _{\beta *}$$ . Combining these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction $$\rightarrow _{\beta \sigma }$$ is used to define a cut elimination procedure for predicate subtyping. This definition provides a new tool to study the properties of predicate subtyping, as illustrated with a proof of consistency.


title: A Process Algebra for Link Layer Protocols

authors:
Rob van Glabbeek
Peter Höfner
Michael Markl

abstract: We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.


title: An Abstract Domain for Trees with Numeric Relations

authors:
Matthieu Journault
Antoine Miné
Abdelraouf Ouadjaout

abstract: We present an abstract domain able to infer invariants on programs manipulating trees. Trees considered in the article are defined over a finite alphabet and can contain unbounded numeric values at their leaves. Our domain can infer the possible shapes of the tree values of each variable and find numeric relations between: the values at the leaves as well as the size and depth of the tree values of different variables. The abstract domain is described as a product of (1) a symbolic domain based on a tree automata representation and (2) a numerical domain lifted, for the occasion, to describe numerical maps with potentially infinite and heterogeneous definition set. In addition to abstract set operations and widening we define concrete and abstract transformers on these environments. We present possible applications, such as the ability to describe memory zones, or track symbolic equalities between program variables. We implemented our domain in a static analysis platform and present preliminary results analyzing a tree-manipulating toy-language.


title: Safe Deferred Memory Reclamation with Types

authors:
Ismail Kuru
Colin S. Gordon

abstract: Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are not deallocated immediately, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. We present a static type system to ensure correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.


title: Effectful Normal Form Bisimulation

authors:
Ugo Dal Lago
Francesco Gavazzo

abstract: Normal form bisimulation, also known as open bisimulation, is a coinductive technique for higher-order program equivalence in which programs are compared by looking at their essentially infinitary tree-like normal forms, i.e. at their Böhm or Lévy-Longo trees. The technique has been shown to be useful not only when proving metatheorems about $$\lambda $$ -calculi and their semantics, but also when looking at concrete examples of terms. In this paper, we show that there is a way to generalise normal form bisimulation to calculi with algebraic effects, à la Plotkin and Power. We show that some mild conditions on monads and relators, which have already been shown to guarantee effectful applicative bisimilarity to be a congruence relation, are enough to prove that the obtained notion of bisimilarity, which we call effectful normal form bisimilarity, is a congruence relation, and thus sound for contextual equivalence. Additionally, contrary to applicative bisimilarity, normal form bisimilarity allows for enhancements of the bisimulation proof method, hence proving a powerful reasoning principle for effectful programming languages.


title: Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms

authors:
Guido Martínez
Danel Ahman
Victor Dumitrescu
Nick Giannarakis
Chris Hawblitzel
Catalin Hritcu
Monal Narasimhamurthy
Zoe Paraskevopoulou
Clément Pit-Claudel
Jonathan Protzenko
Tahina Ramananandro
Aseem Rastogi
Nikhil Swamy

abstract: We introduce Meta-F $$^{\star }$$ , a tactics and metaprogramming framework for the F $$^\star $$ program verifier. The main novelty of Meta-F $$^\star $$ is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F $$^\star $$ can be used to generate verified code automatically. Meta-F $$^\star $$ is implemented as an F $$^\star $$ effect, which, given the powerful effect system of F $$^{\star }$$ , heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F $$^\star $$ type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F $$^\star $$ provides substantial gains in proof development, efficiency, and robustness.


title: Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order

authors:
Dylan McDermott
Alan Mycroft

abstract: Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs. We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language. We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.


title: Time Credits and Time Receipts in Iris

authors:
Glen Mével
Jacques-Henri Jourdan
François Pottier

abstract: We present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program’s execution time, time receipts can be used to establish a lower bound. More strikingly, time receipts can be used to prove that certain undesirable events—such as integer overflows—cannot occur until a very long time has elapsed. We present several machine-checked applications of time credits and time receipts, including an application where both concepts are exploited.


title: Robustly Safe Compilation

authors:
Marco Patrignani
Deepak Garg

abstract: Secure compilers generate compiled code that withstands many target-level attacks such as alteration of control flow, data leaks or memory corruption. Many existing secure compilers are proven to be fully abstract, meaning that they reflect and preserve observational equivalence. Fully abstract compilation is strong and useful but, in certain cases, comes at the cost of requiring expensive runtime constructs in compiled code. These constructs may have no relevance for security, but are needed to accommodate differences between the source and target languages that fully abstract compilation necessarily needs. As an alternative to fully abstract compilation, this paper explores a different criterion for secure compilation called robustly safe compilation or RSC . Briefly, this criterion means that the compiled code preserves relevant safety properties of the source program against all adversarial contexts interacting with the compiled program. We show that RSC can be proved more easily than fully abstract compilation and also often results in more efficient code. We also develop two illustrative robustly-safe compilers and, through them, illustrate two different proof techniques for establishing that a compiler attains RSC . Based on these, we argue that proving RSC can be simpler than proving fully abstraction.


title: A Categorical Model of an \mathbf i/o -typed \pi -calculus

authors:
Ken Sakayori
Takeshi Tsukada

abstract: This paper introduces a new categorical structure that is a model of a variant of the $$ \mathbf {i/o} $$ -typed $$ \pi $$ -calculus, in the same way that a cartesian closed category is a model of the $$ \lambda $$ -calculus. To the best of our knowledge, no categorical model has been given for the $$ \mathbf {i/o} $$ -typed $$ \pi $$ -calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate the relevance of the categorical model, we show by a semantic consideration that the $$ \pi $$ -calculus is equivalent to a core calculus of Concurrent ML.


title: Handling Polymorphic Algebraic Effects

authors:
Taro Sekiyama
Atsushi Igarashi

abstract: Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism that allows abstracting not only expressions but also effects and handlers. Although polymorphism makes it possible to reuse and reason about effect implementations more effectively, it has long been known that a naive combination of polymorphic effects and let-polymorphism breaks type safety. Although type safety can often be gained by restricting let-bound expressions—e.g., by adopting value restriction or weak polymorphism—we propose a complementary approach that restricts handlers instead of let-bound expressions. Our key observation is that, informally speaking, a handler is safe if resumptions from the handler do not interfere with each other. To formalize our idea, we define a call-by-value lambda calculus $$\lambda _\text {eff}^\text {let}$$ that supports let-polymorphism and polymorphic algebraic effects and handlers, design a type system that rejects interfering handlers, and prove type safety of our calculus.


title: One Step at a Time - A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts

authors:
Ferdinand Vesely
Kathleen Fisher

abstract: Big-step and small-step are two popular flavors of operational semantics. Big-step is often seen as a more natural transcription of informal descriptions, as well as being more convenient for some applications such as interpreter generation or optimization verification. Small-step allows reasoning about non-terminating computations, concurrency and interactions. It is also generally preferred for reasoning about type systems. Instead of having to manually specify equivalent semantics in both styles for different applications, it would be useful to choose one and derive the other in a systematic or, preferably, automatic way. Transformations of small-step semantics into big-step have been investigated in various forms by Danvy and others. However, it appears that a corresponding transformation from big-step to small-step semantics has not had the same attention. We present a fully automated transformation that maps big-step evaluators written in direct style to their small-step counterparts. Many of the steps in the transformation, which include CPS-conversion, defunctionalisation, and various continuation manipulations, mirror those used by Danvy and his co-authors. For many standard languages, including those with either call-by-value or call-by-need and those with state, the transformation produces small-step semantics that are close in style to handwritten ones. We evaluate the applicability and correctness of the approach on 20 languages with a range of features.


title: Composing Bidirectional Programs Monadically

authors:
Li-yao Xia
Dominic Orchard
Meng Wang

abstract: Software frequently converts data from one representation to another and vice versa. Naïvely specifying both conversion directions separately is error prone and introduces conceptual duplication. Instead, bidirectional programming techniques allow programs to be written which can be interpreted in both directions. However, these techniques often employ unfamiliar programming idioms via restricted, specialised combinator libraries. Instead, we introduce a framework for composing bidirectional programs monadically, enabling bidirectional programming with familiar abstractions in functional languages such as Haskell. We demonstrate the generality of our approach applied to parsers/printers, lenses, and generators/predicates. We show how to leverage compositionality and equational reasoning for the verification of round-tripping properties for such monadic bidirectional programs.


title: RustHorn: CHC-Based Verification for Rust Programs

authors:
Yusuke Matsushita
Takeshi Tsukada
Naoki Kobayashi

abstract: Abstract Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.