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

from Type Theory Forall · host Pedro Abreu

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

Episode metadata supplied by the publisher feed · Published Apr 2, 2022

Embed this episode

Attribution link and audio player

NOW PLAYING

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

0:00 1:35:53

1×

No transcript for this episode yet

We transcribe on demand. Request one and we'll notify you when it's ready — usually under 10 minutes.

Share this episode

Similar Episodes

No similar episodes found.

Similar Podcasts

No similar podcasts found.

Frequently Asked Questions

How long is this episode of Type Theory Forall?

This episode is 1 hour and 35 minutes long.

When was this Type Theory Forall episode published?

This episode was published on April 2, 2022.

Can I download this Type Theory Forall episode?

Yes. Use the download control on the episode player to save the publisher-provided media file.

URL copied to clipboard!