Programming Languages
Although timing and synchronization of a dynamically-changing set of elements and their related power considerations are essential to many cyber-physical systems (CPS), they are absent from today's programming languages, forcing programmers…
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the…
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…
The Isabelle proof assistant includes a small functional language, which allows users to write and reason about programs. So far, these programs could be extracted into a number of functional languages: Standard ML, OCaml, Scala, and…
Programming language frameworks allow us to generate language tools (e.g., interpreters) just from a formal description of the syntax and semantics of a programming language. As these frameworks tend to be quite complex, an issue arises…
Reactive graphs are transition structures whereas edges become active and inactive during its evolution, that were introduced by Dov Gabbay from a mathematical's perspective. This paper presents Marge (https://fm-dcc.github.io/MARGe), a…
Multiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this paper, we extend a minimal MPST system with quantum data and…
We advance the thesis that the simulation of quantum circuits is fundamentally about the efficient management of a large (potentially exponential) number of delimited continuations. The family of Scheme languages, with its efficient…
LMNtal is a programming and modeling language based on hierarchical graph rewriting that uses logical variables to represent connectivity and membranes to represent hierarchy. On the theoretical side, it allows logical interpretation based…
TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level…
Data-flow analyses like points-to analysis can vastly improve the precision of other analyses, and help perform powerful code optimizations. However, whole-program points-to analysis of large programs tend to be expensive - both in terms of…
The choice of how to represent an abstract type can have a major impact on the performance of a program, yet mainstream compilers cannot perform optimizations at such a high level. When dealing with optimizations of data type…
The miniKanren and Relational Programming Workshop is a workshop for the miniKanren family of relational (pure constraint logic programming) languages: miniKanren, microKanren, core.logic, OCanren, Guanxi, etc. The workshop solicits papers…
Formal mathematics and computer science proofs are formalized using Hilbert-Russell-style logical systems which are designed to not admit paradoxes and self-refencing reasoning. These logical systems are natural way to describe and reason…
To take full advantage of a specific hardware target, performance engineers need to gain control on compilers in order to leverage their domain knowledge about the program and hardware. Yet, modern compilers are poorly controlled, usually…
Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be…
We consider the verification of omega-regular linear temporal properties of concurrent programs running under weak memory semantics. We observe that in particular, these properties may enforce liveness clauses, whose verification in this…
Concurrent computations resemble conversations. In a conversation, participants direct utterances at others and, as the conversation evolves, exploit the known common context to advance the conversation. Similarly, collaborating software…
Using standard components of modern Fortran we present a technique to dynamically generate strings with as little coding overhead as possible on the application side. Additionally we demonstrate how this can be extended to allow for output…
Pawns is a programming language under development which supports pure functional programming (including algebraic data types, higher order programming and parametric polymorphism) and imperative programming (including pointers, destructive…