diff --git a/podcast/75/index.markdown b/podcast/75/index.markdown
new file mode 100644
index 00000000..a16fa835
--- /dev/null
+++ b/podcast/75/index.markdown
@@ -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.
diff --git a/podcast/75/links.markdown b/podcast/75/links.markdown
new file mode 100644
index 00000000..eb8afaae
--- /dev/null
+++ b/podcast/75/links.markdown
@@ -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)
+