976 papers · page 1 of 49
Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring correctness of RDMA programs has only recently become possible with the formalisation of rdmatso sema…
We propose the integration of staged metaprogramming into a session-typed message passing functional language. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may be boxed …
Abstract We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of $$\textsf{MLTT}$$ MLTT , we show that they inductively approximate idealized functional objects as decision trees, realizing a generalized form of continuity. …
Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect system…
Abstract Program equivalence is the heart of reasoning about and proving properties of programs. To assert noninterference, for example, a program is shown to be equivalent to itself up to the confidentiality level of an observer. A powerful enabler for such proofs are logical re…
Abstract Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running e…
Abstract We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad $$T(- \oplus E)$$ T ( - ⊕ E ) in a linear setting. We consider in particular for T the allocat…
We make the case that the foundation for Rely-Guarantee reasoning can be fruitfully delivered by a coinductive semantics. Using insight from an Isabelle formalization, via a proof analysis we show that the coinductive semantics tends to simplify the proof development; in particul…
Commutativity reasoning based on Lipton’s movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a subset of the initial set of interleavings, which is sound modulo reorderings of commutative actions. …
Abstract Symbolic execution is a popular program analysis technique that has been successfully used for bug-finding and bounded verification in various modern programming languages. Despite its popularity, however, symbolic execution suffers from two main limitations when applied…
A fundamental computational task in probabilistic programming is to infer a program’s output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. While most …
Understanding and predicting the worst-case resource usage is crucial for software quality; however, existing methods either over-approximate with potentially loose bounds or under-approximate without asymptotic guarantees. This paper presents a program logic to under-approximate…
The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. We may think of digital twins not merely as models, but as systems for model management, integration, and composition. In fact, digital twins are model-centric …
We investigate the precise consistency guarantees provided by a simple and prominent distributed implementation of shared memory (a.k.a. key-value store) based on the causal broadcast abstraction. We formalize these guarantees within a weak memory model, which we call “causal-bro…
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning about effectful computations. However, exis…
Abstract Lazy evaluation offers great flexibility by computing only what is necessary. However, analysing the cost of lazy programs is notoriously challenging, as computation occurs out of order and depends on future demands. Recent work has proposed alternative semantics for mod…
One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with distinct features. These state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to program co…
We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of co…