PRS Group @ TU Darmstadt - Andrés Goens
Marcus Rossel

Marcus Rossel

Marcus completed his MSc in computer science at Technische Universität Dresden with a focus on formal methods. He joined the PRS group as a PhD student in 2026 and is working mainly on automation in interactive theorem provers. This work touches on topics such as meta-programming, rewriting, and logics.

Publications

  1. POPL'26 Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation

    Marcus Rossel, Rudi Schneider, Thomas Koehler, Michel Steuwer, Andrés Goens

  2. PLDI'25 Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs

    Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andrés Goens, Thomas Koehler, Michel Steuwer

  3. ARXIV'25 The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

    Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng

  4. EGRAPHS'24 Bridging Syntax and Semantics of Lean Expressions in E-Graphs

    Marcus Rossel, Andrés Goens

  5. VSTTE'23 Provable Determinism for Software in Cyber-Physical Systems

    Marcus Rossel, Shaokai Lin, Marten Lohstroh, Jerónimo Castrillón, Andrés Goens