I'm a PhD student at ETH Zürich in Computer Science.
My advisor is Ralf Jung and I work on logics for reasoning about programs.
Previously, I did a MSc in pure mathematics
at the University of Copenhagen.
Here, you can find my research in math and CS.
.
GPG.
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.