This website is no longer maintained; you can find more up-to-date information on my new website.
I received my BA in Computer Science from Saarland University in 2014 and a Master of Philosophy in Advanced Computer Science from the University of Cambridge in 2015.
I am interested in how we can close the gaps between mechanised proofs and their traditional paper-based counterpart. During my time at the Programming Systems Lab, I worked on supporting binders in the general-purpose proof assistant Coq. In my thesis, I developed the Autosubst 2 tool, which generates binder boilerplate for many-sorted, variadic, and modular syntax.
I am now a Presidential Postdoctoral Research Fellow in the group of Andrew Appel at Princeton University (This is my new website).
Coq à la Carte - A Practical Approach to Modular Syntax with Binders (pdf, slides, video)
Yannick Forster and Kathrin Stark
CPP 2020, New Orleans, USA, 2020.
POPLMark reloaded: Mechanizing proofs by logical relations (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.
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.
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)
Gert Smolka, Kathrin Stark
ITP 2016, Nancy, France, 2016.
Ph.D. Thesis: Mechanising Syntax with Binders in Coq (Advisor: Prof. Gert Smolka)
Research Essay for the Master: Towards a Compuational Interpretation of Homotopy Type Theory (Advisor: Prof. Timothy G. Griffin)
Bachelor Thesis: Quantitative Recursion-Free Process Axiomatization in Coq (Advisor: Prof. Dr. Holger Hermanns)
Sarah Mameche, 2018, Bachelor's thesis
Autosubst: Automation for de Bruijn substitutions in Lean
| Summer 2019 | Advisor Funktionale Programmierung Proseminar, Programming Systems Lab. |
| Summer 2018 | Lecturer and Advisor Advanced Coq Programming Block Lecture, Programming Systems Lab. |
| Summer 2018 | Advisor Funktionale Programmierung Proseminar, Programming Systems Lab. |
| Winter 2017 | TA Semantics Lecture, Programming Systems Lab. |
| Winter 2017 | Organiser/Advisor Category Theory Seminar, Programming Systems Lab. |
| Summer 2017 | Advisor Category Theory Seminar, Programming Systems Lab. |
| Winter 2016 | Advisor Funktionale Programmierung Proseminar, Programming Systems Lab. |
| Summer 2016 | TA Introduction to Computational Logic Lecture, Programming Systems Lab. |
| Summer 2016 | Advisor Computational Logic Seminar, Programming Systems Lab. |
Kathrin Stark, Ph.D.
Postdoctoral Research Fellow
Princeton University
35 Olden Street
08540 Princeton
Phone: ++1 - (609) - 258 0451
E-Mail: kstark@princeton.edu