Skip to content

Haskell Interlude #75: Kathrin Stark #566

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
LaurentRDC merged 1 commit into from
Jan 12, 2026
Merged

Haskell Interlude #75: Kathrin Stark #566

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions podcast/75/index.markdown
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
title: Kathrin Stark
episode: 75
buzzsproutId: 18487464
recorded: 2025-10-10
published: 2026-01-11
---

We are joined by Kathrin Stark, a professor at Heriot-Watt University
in Edinburgh. Kathrin works on program verification with proof
assistants, so her focus is not exactly on Haskell, but on topics dear
to Haskellers' hearts such as interactive theorem provers, writing
correct programs, and the activities needed to produce them. We
discuss many aspects of proofs and specifications, and the languages
involved in the process, as well as verifying and producing provably
correct neural networks.
18 changes: 18 additions & 0 deletions podcast/75/links.markdown
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
- [Kathrin's home page](https://www.k-stark.de/)
- [Scottish Programming Languages Seminar Series (SPLS)](https://spli.scot/spls/)
- [SPLV25: Scottish Programming Languages and Verification Summer School 2025](https://spli.scot/splv/2025-edinburgh/)
- [Paper: Data types à la carte](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/data-types-a-la-carte/14416CB20C4637164EA9F77097909409)
- [Paper: A Verified Foreign Function Interface Between Coq and C](https://popl25.sigplan.org/details/POPL-2025-popl-research-papers/24/A-Verified-Foreign-Function-Interface-Between-Coq-and-C)
- [Paper: Verified Neural Networks](https://arxiv.org/abs/2405.10611)
- [CompCert (verified C compiler)](https://compcert.org/)
- [CertiCoq: A verified compiler for Coq](https://certicoq.org/)
- [VST (Verified Software Toolchain)](https://vst.cs.princeton.edu/)
- [Isabelle (proof assistant)](https://isabelle.in.tum.de/), [its language Isar](https://isabelle.in.tum.de/Isar/)
- [Paper: Logic of Differentiable Logics: Towards a Uniform Semantics of DL](https://arxiv.org/abs/2303.10650)
- [Paper: Modular type-safety proofs in Agda](https://dl.acm.org/doi/10.1145/2428116.2428120)
- [Paper: Meta-theory à la carte](https://dl.acm.org/doi/abs/10.1145/2429069.2429094)
- [Paper: Generic datatypes à la carte](https://dl.acm.org/doi/10.1145/2502488.2502491)
- [Paper: Modular monadic meta-theory](https://dlnext.acm.org/doi/10.1145/2500365.2500587)
- [Paper: Extensible Metatheory Mechanization via Family Polymorphism](https://dl.acm.org/doi/10.1145/3591286)
- [Paper: Certified Compilers à la Carte](https://dl.acm.org/doi/10.1145/3729261)