Fique off-line com o app Player FM !
#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx
Manage episode 420953630 series 2951423
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
82 episódios
Manage episode 420953630 series 2951423
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
82 episódios
Wszystkie odcinki
×Bem vindo ao Player FM!
O Player FM procura na web por podcasts de alta qualidade para você curtir agora mesmo. É o melhor app de podcast e funciona no Android, iPhone e web. Inscreva-se para sincronizar as assinaturas entre os dispositivos.