Player FM uygulamasıyla çevrimdışı 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 bölüm
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 bölüm
ทุกตอน
×Player FM'e Hoş Geldiniz!
Player FM şu anda sizin için internetteki yüksek kalitedeki podcast'leri arıyor. En iyi podcast uygulaması ve Android, iPhone ve internet üzerinde çalışıyor. Aboneliklerinizi cihazlar arasında eş zamanlamak için üye olun.