I am a Presidential Postdoctoral Research Fellow at Princeton University in the group of Andrew Appel, where I work on a verified interface between CertiCoq and VST. I received my PhD in Computer Science from Saarland University in February 2020, where I developed the Autosubst 2 tool and was part of the Programming Systems Lab of Gert Smolka. I previously lived and studied in Saarbrücken and Cambridge.
My research evolves around programs and proofs, developed with interactive proof assistants, such as Coq. These tools allow and simplify the development of indisputable proofs in an interplay between humans and computers. While they are guaranteed to be correct, mechanized proofs often still involve a considerable overhead compared to traditional paper-based proofs.
My goal is to both construct such proofs and to minimize this overhead in a principled way.
Since the start of my studies (and thanks to having had excellent teachers and mentors), I have further been passionate about teaching students, teaching how to teach, and getting the ideas of computer science (and theorem proving in particular) to a broader audience.
July 2020 - I am part of the CoqPL 2021 Programm Committee.
April 2020 - I am part of the CPP 2021 Programm Committee.
February 2020 - I defended my dissertation on mechanising syntax with binders and Autosubst 2. A big thanks to the examination board, consisting of Markus Bläser, Roland Leißa, Brigitte Pientka, and my advisor Gert Smolka!
POPLMark reloaded: Mechanizing proofs by logical relations (pdf of preprint, website)
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
Journal of Functional Programming, Volume 29, 2019.
Extended Abstracts and Talks
I used to be TA, head TA, advisor, organizer, and lecturer for a wide range of lectures and seminars at Saarland University.
Summer 2019 - Advisor for Funktionale Programmierung, Proseminar, Programming Systems Lab.
Summer 2018 - Organizer and Advisor for Funktionale Programmierung, Proseminar, Programming Systems Lab.
Summer 2018 - Lecturer and Advisor for Advanced Coq Programming, Block Lecture, Programming Systems Lab.
Winter 2017 - Teaching Assistant for Semantics, Lecture, Programming Systems Lab.
Winter 2017 - Organizer and Advisor for Category Theory, Seminar, Programming Systems Lab.
Summer 2017 - Advisor for Category Theory, Seminar, Programming Systems Lab.
Winter 2016 - Advisor for Funktionale Programmierung, Proseminar, Programming Systems Lab.
Summer 2016 - Teaching Assistant for Introduction to Computational Logic, Lecture, Programming Systems Lab.
Summer 2016 - Advisor for Computational Logic, Seminar, Programming Systems Lab.
Selected Outreach Activities
I had the luck to stumble into Computer Science - but believe school often fails to transfer a realistic picture of computer science early on.
Contact me if you want to hear more about the contents or organization of any of these events.
May 2019 - Two invited lectures on theorem proving and category theory for the Fachschaftstagung “Moderne Programmierkonzepte” of the Cusanuswerk (a meeting for Ph.D. students of a German scholarship organization).
2017 - 2018 - Organizer and lecturer of each three 4-hour courses “Interactive Theorem Proving” for the “Saarbrücker Forschungstage” (Saarbrücken Research days, a seminar for the best pupils in a German computer science competition).
2012-2017 - Depending on the year, tutor, organizer, lecturer, and/or coach for the four-weeks Mathematics Preparatory Class of Saarland University on a voluntary basis. The course won the BeStE Award for Student Initiatives and Extraordinary Commitment, awarded by the university's presidential board.
Organized and led the tutor workshops for this course and Programming 1 until 2019.