Programming Languages
Building on the successes of satisfiability modulo theories (SMT), Bj{\o}rner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained…
This volume contains the formal proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), held on 8th of Juli 2018 in Oxford, United Kingdom, and affiliated with FLoC 2018…
Gradual typing enables programmers to combine static and dynamic typing in the same language. However, ensuring a sound interaction between the static and dynamic parts can incur significant runtime cost. In this paper, we perform a…
Software frequently converts data from one representation to another and vice versa. Naively specifying both conversion directions separately is error prone and introduces conceptual duplication. Instead, bidirectional programming…
We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on…
Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect.…
Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of data-types: we can finally write correct-by-construction software. However, this extreme accuracy is also a…
Transient gradual typing imposes run-time type tests that typically cause a linear slowdown in programs' performance. This performance impact discourages the use of type annotations because adding types to a program makes the program…
Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its variants simultaneously in a single run by exploiting the…
Our community believes that new domain-specific languages should be as general as possible to increase their impact. However, I argue in this essay that we should stop claiming generality for new domain-specific languages. More general…
Yarel is a core reversible programming language that implements a class of permutations, defined recursively, which are primitive recursive complete. The current release of Yarel syntax and operational semantics, implemented by compiling…
We propose a calling convention for capability machines with local capabilities. The calling convention ensures local-state encapsulation and well-bracketed control flow. We use the calling convention in a hand-full of program examples and…
Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite…
The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages. This paper explores speculative side-channel attacks and their…
This dissertation is concerned with the study of program equivalence and algebraic effects as they arise in the theory of programming languages. Algebraic effects represent impure behaviour in a functional programming language, such as…
Modern microprocessors are equipped with Single Instruction Multiple Data (SIMD) or vector instructions which expose data level parallelism at a fine granularity. Programmers exploit this parallelism by using low-level vector intrinsics in…
Rust is a popular programming language in building various low-level software in recent years. It aims to provide safe concurrency when implementing multi-threaded software through a suite of compiler checking rules. Unfortunately, there is…
The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and…
Graph-based data models allow for flexible data representation. In particular, semantic data based on RDF and OWL fuels use cases ranging from general knowledge graphs to domain specific knowledge in various technological or scientific…
During its lifetime, a program suffers several changes that seek to improve or to augment some parts of its functionality. However, these modifications usually also introduce errors that affect the already-working code. There are several…