Programming Languages
There are a lot of different programming paradigms. Since all Turing-complete programming languages are formally equivalent (they have the same ability to express any computable problem), the existence of so many different paradigms may…
Common functional languages incentivize tail-recursive functions, as opposed to general recursive functions that consume stack space and may not scale to large inputs. This distinction occasionally requires writing functions in a…
We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers \`a la Dijkstra and through the lens of Kleene algebra with top…
First-order logic (FOL) has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as heap-manipulating programs and distributed protocols, FOL,…
Reductions combine collections of inputs with an associative (and here, also commutative) operator to produce collections of outputs. When the same value contributes to multiple outputs, there is an opportunity to reuse partial results,…
Structure editors operate directly on a program's syntactic tree structure. At first glance, this allows for the exciting possibility that such an editor could enforce correctness properties: programs could be well-formed and sometimes even…
Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have…
Algebraic effects & handlers have become a standard approach for side-effects in functional programming. Their modular composition with other effects and clean separation of syntax and semantics make them attractive to a wide audience.…
Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling…
The transition from x86 to ARM architecture is becoming increasingly common across various domains, primarily driven by ARM's energy efficiency and improved performance across traditional sectors. However, this ISA shift poses significant…
Building a high-performance JIT-capable VM for a dynamic language has traditionally required a tremendous amount of time, money, and expertise. We present Deegen, a meta-compiler that allows users to generate a high-performance JIT-capable…
Many of today's message-passing systems not only require messages to be exchanged in a certain order but also to happen at a certain \emph{time} or within a certain \emph{time window}. Such correctness conditions are particularly prominent…
We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are…
Dataflow analysis is a fundamental code analysis technique that identifies dependencies between program values. Traditional approaches typically necessitate successful compilation and expert customization, hindering their applicability and…
Relational object invariants (or representation invariants) are relational properties held by the fields of a (memory) object throughout its lifetime. For example, the length of a buffer never exceeds its capacity. Automatic inference of…
We study the data-parallel language BUTF, inspired by the Futhark language for array programming. We give a translation of BUTF into a version of the pi-calculus with broadcasting and labeled names. The translation is both complete and…
Many type systems have been presented in the literature for variants of the pi-calculus, but none of them are able to handle composite subjects such as those found in the language epi, which features polyadic synchronisation. The purpose of…
We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method…
Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of…
Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the…