I'm a doctoral student at ETH Zürich in Computer Science.
My advisor is Ralf Jung and I work on logics for reasoning about programs.
Previously, I completed a MSc in pure mathematics
at the University of Copenhagen
and then taught CS there.
Here, you can find my research in math and CS.
.
GPG.
Abstract: Program logics have proven effective at verifying programs by leveraging modular reasoning. However, the process of building program logics is itself usually not modular: Even though many languages share common features like integers, booleans, heaps, or concurrency, program logics for different languages are usually defined and proven sound independently. In this paper, we present Mosaic, a new framework for building program logics by composition. Mosaic views a programming language as a sum of fragments. Each fragment covers a particular feature or aspect of a language, supplying syntax, semantics, program logic, and soundness of said logic. These fragments can be freely combined to obtain a programming language with an accompanying program logic. When realized in a proof assistant, each fragment furthermore comes with a set of tactics that are then automatically available in any language that includes the fragment. We provide a library of 27 fragments, including fragments for higher-order heaps, concurrency, and atomic blocks. Particularly noteworthy is our fragment for prophecy variables which comes with a reusable, language-generic erasure theorem. To demonstrate the scalability of our approach, we use it to recreate the HeapLang and λRust languages from prior work. We show that our composed versions are usable in practice by porting several large proof examples with minimal changes. All of our development is formalized using Rocq and Iris.
Abstract: Program logics have proven a successful strategy for verification of complex programs. By providing local reasoning and means of abstraction and composition, they allow reasoning principles for individual components of a program to be combined to prove guarantees about a whole program. Crucially, these components and their proofs can be reused. However, this reuse is only available once the program logic has been defined. It is a frustrating fact of the status quo that whoever defines a new program logic must establish every part, both semantics and proof rules, from scratch. In spite of programming languages and program logics typically sharing many core features, reuse is generally not available across languages. Even inside one language, if the same underlying operation appears in multiple language primitives, reuse is typically not possible when establishing proof rules for the program logic. To enable reuse across and inside languages when defining complex program logics (and proving them sound), we serve program logics à la carte by combining program logic fragments for the various effects of the language. Among other language features, the menu includes shared state, concurrency, and non-determinism as reusable, composable blocks that can be combined to define a program logic modularly. Our theory builds on ITrees as a framework to express language semantics and Iris as the underlying separation logic; the work has been mechanized in the Coq proof assistant.
Abstract: We give a new proof of homological stability with the best known isomorphism range for mapping class groups of surfaces with respect to genus. The proof uses the framework of Randal-Williams—Wahl and Krannich applied to disk stabilization in the category of bidecorated surfaces, using the Euler characteristic instead of the genus as a grading. The monoidal category of bidecorated surfaces does not admit a braiding, distinguishing it from previously known settings for homological stability. Nevertheless, we find that it admits a suitable Yang—Baxter element, which we show is sufficient structure for homological stability.
Abstract: Using the Galatius—Kupers—Randal-Williams framework of cellular E2-algebras, we prove a secondary stability theorem for mapping class groups of nonorientable surfaces. As a corollary, we obtain a new best known stability range for the homology of the mapping class groups of nonorientable surfaces with respect to adding torus holes.
Abstract: We present new techniques for synthesizing programs through sequences of mutations. Among these are (1) a method of local scoring assigning a score to each expression in a program, allowing us to more precisely identify buggy code, (2) suppose-expressions which act as an intermediate step to evolving if-conditionals, and (3) cyclic evolution in which we evolve programs through phases of expansion and reduction. To demonstrate their merits, we provide a basic proof-of-concept implementation which we show evolves correct code for several functions manipulating integers and lists, including some that are intractable by means of existing Genetic Programming techniques.