#17 The Lost Elegance of Computation
May 9th 2022
Conal Elliott
#16 Agda, K Axiom, HoTT, Rewrite Theory
April 2nd 2022
Jesper Cockx
in this episode we interview Jesper Cockx, one of the core developers on Agda. We talk about the philosophy behind Agda, his work on pattern matching, the Uniqueness of Identity of Proofs, UIP for short, and why it is inconsistent with Homotopy Type Theory.
Links
- Jesper’s Website
- Jesper’s Twitter: @agdakx
- Jesper’s PhD Thesis
- Rewrite Theory paper
- Pattern matching without K paper (Check his website for more)
- EuroProofNet
- WITS Talks on Youtube (Workshop on the Implementation of Type Systems)
- Agda Zulip
- Agda Mailing List
- Ataca Github
- Wadler’s book on Agda
- Stump’s book on Agda
Tweet