CV ⋄ Mail ⋄ Google Scholar ⋄ dblp

I just started a new position as 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

February 2022 - I just started a new position as an assistant professor at Heriot-Watt University.

January 2021 - I won the Amazing Reviewer Award of CPP 2021!

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!

January 2020 - I attended CoqPL/CPP/POPL 2020 - happy to have given a keynote at CoqPL and to have presented our paper on modular syntax in Coq at CPP, check it out!

January 2020 - I started as a Presidential Postdoctoral Research Fellow at Princeton University in the group of Andrew Appel.

Research

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

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

2021 - Program Committee CPP 2021.

2020 - Program Committee CPP 2020.

External Reviewer for ITP 2018, JPF 2019.

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

2018 - Bachelor Thesis of Sarah Mameche, Autosubst: Automation for de Bruijn substitutions in Lean.

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

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