976 papers · page 3 of 49
Abstract Replication is an alternative construct to recursion for describing infinite behaviours in the $$\pi $$ π -calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-pa…
Abstract A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type axiom. In this work, we argue that a universe hierarchy is not t…
Abstract Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or uni…
Abstract Variable Elimination ( $$\textsf{VE}$$ VE ) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Eli…
Abstract Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating …
Abstract Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic supporting thread-l…
Abstract "Image missing""Image missing" Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised mul…
Abstract Recurrence relations are used in a wide variety of static program analysis tasks such as loop summarization, invariant generation, and, most classically, modeling the (asymptotic) worst-case runtime behavior of recursive divide-and-conquer algorithms. In this work, we fo…
Abstract Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs inten…
Abstract Choreographic programming (CP) is a method to implement distributed systems that ensures communication deadlock freedom by design. To use CP, though, the number of processes and the network among them must be known statically. Often, that information is known only dynami…
Abstract Algorithmic versions of the Lovász Local Lemma (ALLLs), or rather, the Moser-Tardos algorithm and its variants, are impactful in both theory and practice. In this paper, we take the first step towards the goal of formally verifying ALLLs by applying programming language …
Abstract We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiment, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the exist…
International audience
Abstract We introduce a sound and complete equational theory capturing equivalence of discrete probabilistic programs, that is, programs extended with primitives for Bernoulli distributions and conditioning, to model distributions over finite sets of events. To do so, we translat…
Abstract Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we addre…
Abstract Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written in the Prelude/…
Abstract In this paper, we consider specific dataflow solvers, inspired by the work of Bourdoncle [5], in which an iteration order is pre-computed, based on the structure of the control-flow graph of programs. Our work aims at a clearer formulation and a better understanding of t…
Abstract In this report, we provide our full set of results for the experimental evaluation of our formally verified, WTO-based dataflow solvers [2]. We also detail useful information regarding our artifact [3] and evaluation setup. In particular, we validate experimentally that …
Abstract Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That …
Abstract We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as spec…