#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

Type Theory Forall - A podcast by Pedro Abreu

Try Bookbeat 60! days for free, click here

Try Bookbeat 60! days for free, click here

Enjoy a whole world of audiobooks and e-books, everything from new releases to the classics

 Sponsored

Categories:

Technology

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

Visit the podcast's native language site