add episode 20

Author: nikivazou

podcast/20/index.markdown

@@ -0,0 +1,8 @@
+---
+title: Jesper Cockx
+episode: 20
+buzzsproutId: 12051036
+recorded: 2022-12-28
+published: 2023-01-16
+---
+In this episode Jesper Cockx, one of the main Agda developers, is interviews by Niki Vazou and Matthias Pall. They talk about how to explain dependent types to one's father, how Agda’s automation and proof search work, and how Agda can be used to verify Haskell code bases.

podcast/20/links.markdown

@@ -0,0 +1,7 @@
+* [Jesper's website](https://jesper.sikanda.be/)
+* [Jesper's twitter](https://twitter.com/agdakx)
+* [Agda](https://wiki.portal.chalmers.se/agda/Main/HomePage)
+* [Reasonable Agda Is Correct Haskell](https://github.com/agda/agda2hs)
+* [A tutorial for Automated Theorem Proving in Agda](https://link.springer.com/chapter/10.1007/11617990_10)
+* [Liar Paradox](https://en.wikipedia.org/wiki/Liar_paradox)
+* [Workshop on the Implementation of Type Systems](https://popl22.sigplan.org/home/wits-2022)