1,205 papers · page 2 of 61
We develop a session types framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursio…
Notions of computation can be modeled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equi…
This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a …
We present IrisFit, a Separation Logic with space credits for reasoning about heap space in a concurrent call-by-value language equipped with tracing garbage collection and shared mutable state. We point out a fundamental difficulty in the analysis of the worst-case heap space co…
The notion of equality is at the heart of dependent type theory, as it plays a fundamental role in program specifications and mathematical reasoning. In mainstream proof assistants such as Agda , Lean , and Coq , equality is usually defined using Martin-Löf’s identity type, an el…
Inheritance is a key concept in many programming languages. Dynamically typed languages, such as JavaScript, often support powerful forms of dynamic inheritance. However, dynamic inheritance poses significant challenges for static typing. Most statically typed languages only prov…
Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the strong invariant synthesis …
Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs—roughly, they are BDDs augmented with a certain form of procedure call. A natural que…
Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the different kinds of programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution t…
The main goal of most static analyses is to prove the absence of bugs : if the analysis reports no alarms, then the program will not exhibit any unwanted behaviours. For this reason, they are designed to over-approximate program behaviours and, consequently, they can report some …
This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as transition systems. The implem…
Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, wh…
Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used i…
Robustness is a key and desirable property of any classifying system, in particular, to avoid the ever-rising threat of adversarial attacks. Informally, a classification system is robust when the result is not affected by the perturbation of the input. This notion has been extens…
Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into execut…
Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The…
We introduce layering to modal type theory to support meta-programming and intensional analysis coherently. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed λ -calculus with no modalit…
Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide developers in designing efficient algorithms, but it can still be difficult to apply algorithmic paradigms to practical tasks. To ease the usage of paradigms, many research efforts have been devoted to t…
Big data analytics frameworks, such as Spark and Giraph, need to process and cache massive datasets that do not always fit on the managed heap. Therefore, frameworks temporarily move long-lived objects outside the heap (off-heap) on a fast storage device. However, this practice r…