Embedded Files
I am currently an assistant professor at Heriot-Watt University.
Before, I used to be a Presidential Postdoctoral Research Fellow at Princeton University in the group of Andrew Appel, where I worked 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.
News
News
September 2025 - Submissions for the POPL Research Competition are open.
September 2025 - I will give an invited talk at ITP 2025.
September 2025 - I gave a talk at the EuroProofNet Workshop on Proof Libraries.
June 2025 - Our paper on A Certified Proof Checker for Deep Neural Network Verification in Imandra got accepted at ITP.
January 2025 - I gave an invited talk at TFP 2025.
January 2025 - Joomy Korkut presents our paper on A Verified Foreign Function Interface between Coq and C at POPL 2025.
Research
Research
Publications
Publications
Mechanising Syntax with Binders (pdf, slides)
Kathrin Stark
Ph.D. thesis, Saarland University, 2020.
Coq à la Carte - A Practical Approach to Modular Syntax with Binders (pdf, slides, video)
Yannick Forster, Kathrin Stark
CPP 2020, New Orleans, USA, 2020.
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.
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions (pdf, slides)
Kathrin Stark, Steven Schäfer, Jonas Kaiser
CPP 2019, Cascais, Portugal, 2019.
Call-By-Push-Value in Coq: Operational, Equational and Denotational Theory (pdf)
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
CPP 2019, Cascais, Portugal, 2019.
Binder-Aware Recursion over Well-Scoped de Bruijn Syntax (pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
CPP 2018, Los Angeles, USA, 2018.
Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions (pdf, slides)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
LFMTP 2017, Oxford, UK, 2017.
Finite Sets in Constructive Type Theory (pdf, slides)
Gert Smolka, Kathrin Stark
ITP 2016, Nancy, France, 2016.
Extended Abstracts and Talks
Extended Abstracts and Talks
Autosubst 2: Mechanising Binders in Coq (slides, video).
Keynote at CoqPL 2019.
Embedding Higher-Order Abstract Syntax in Type Theory (pdf)
Steven Schäfer, Kathrin Stark
24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, 2018.
Academic Service
Academic Service
Teaching
Teaching
Selected Teaching
Selected Teaching
I used to be TA, head TA, advisor, organizer, and lecturer for a wide range of lectures and seminars at Saarland University.
Spring 2021 - Preceptor for COS126: Computer Science: An Interdisciplinary Approach, Lecture, Princeton 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.
Supervised Students
Supervised Students
2018 - Bachelor Thesis of Sarah Mameche, Autosubst: Automation for de Bruijn substitutions in Lean.
Selected Outreach Activities
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-2019 - Mentor for female high school students at the MentoMINT program.
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.
Contact
Contact
I am happy to chat about both existing research and potential future projects - get in touch with me on the platform of your choice!
Office: Earl Mountbatten Building, EM1.34, Heriot-Watt University
E-Mail: K.Stark@hw.ac.uk
Mail ⋄ Google Scholar ⋄ dblp
Page updated
Google Sites
Report abuse