#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx
Type Theory Forall
English - April 02, 2022 16:20 - 1 hour - 82.1 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #15 Coq Projects, Agda, Idris, Kind - Nitin and Eric
Next Episode: #17 The Lost Elegance of Computation - Conal Elliott
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