Related papers: Effects and Coeffects in Call-By-Push-Value (Exten…
Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of…
We describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent programming language. We prove the soundness of a number of general effect-based program equivalences, including a…
We propose a call-by-value lambda calculus extended with a new construct inspired by abductive inference and motivated by the programming idioms of machine learning. Although syntactically simple the abductive construct has a complex and…
While modern software development heavily uses versioned packages, programming languages rarely support the concept of versions in their semantics, which makes software updates more bulky and unsafe. This paper proposes a programming…
Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to call-by-value programs. This hides looping bugs from the programmer, and changes the behavior of a program depending on whether it…
Several recently proposed program logics have incorporated notions of underapproximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an…
Computer programs are often factored into pure components -- simple, total functions from inputs to outputs -- and components that may have side effects -- errors, changes to memory, parallel threads, abortion of the current loop, etc. We…
The framework of Light Logics has been extensively studied to control the complexity of higher-order functional programs. We propose an extension of this framework to multithreaded programs with side effects, focusing on the case of…
Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus.…
This paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores to represent the…
The invariance thesis of Slot and van Emde Boas states that all reasonable models of computation simulate each other with polynomially bounded overhead in time and constant-factor overhead in space. In this paper we show that a family of…
There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous - the latter is required to do any serious mathematics. We…
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCF$_{\textsf{v}}$). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental…
In order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program…
In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The theory of decorated logic provides a rigorous for- malism (with…
Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about…
Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability…
A fully-automated algorithm is developed able to show that evaluation of a given untyped lambda-expression will terminate under CBV (call-by-value). The ``size-change principle'' from first-order programs is extended to arbitrary untyped…
This note is about using computational effects for scalability. With this method, the specification gets more and more complex while its semantics gets more and more correct. We show, from two fundamental examples, that it is possible to…
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of Guarded Interaction Trees to support formal reasoning about…