Programming Languages
Nominal techniques provide a mathematically principled approach to dealing with names and variable binding in programming languages. This paper explores an attempt to make nominal techniques accessible as an Agda library. We aim for a…
This work examines approaches to making computational models reversible. Broadly speaking, transforming a computational model into a reversible one, i.e. reversibilizing it, means extending its operational semantics conservatively in a way…
We introduce and study the problem of detecting short races in an observed trace. Specifically, for a race type $R$, given a trace $\sigma$ and window size $w$, the task is to determine whether there exists an $R$-race $(e_1, e_2)$ in…
We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the language. We then define a program transformation applying a…
There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large class of programs and language features. However, non-local…
Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such…
We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus…
The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to…
Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of…
Constant-time (CT) verification tools are commonly used for detecting potential side-channel vulnerabilities in cryptographic libraries. Recently, a new class of tools, called speculative constant-time (SCT) tools, has also been used for…
Large Language Models (LLM) show strong abilities in code generation, but their skill in creating efficient parallel programs is less studied. This paper explores how LLMs generate task-based parallel code from three kinds of input prompts:…
Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions…
Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs.…
Rust is a memory-safe programming language that disallows undefined behavior. Its safety guarantees have been extensively examined by the community through empirical studies, which has led to its remarkable success. However, unsafe code…
Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool…
Choreographies describe distributed protocols from a global viewpoint, enabling correct-by-construction synthesis of local behaviours. We develop a policy-parametric type system that prevents information leaks from high-security data to…
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C. Automatically translating C to Rust is thus an appealing course of action. Several works have gone down this path, handling an…
Large Language Models (LLMs) have shown remarkable capabilities in solving various programming tasks, such as code generation. However, their potential for code optimization, particularly in performance enhancement, remains largely…
AI kernel compilation for edge devices depends on the compiler's ability to exploit parallelism and hide memory latency in the presence of hierarchical memory and explicit data movement. This paper reports a benchmark methodology and…
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof writing. The proof establishes semantic…