#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric
Nitin and Eric
March 27, 20221h 17mExplicit
Audio is streamed directly from the publisher (api.typetheoryforall.com) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
In this episode me, Eric and Nitin continues our conversation started in the last episode. This time we move our attention to the cool projects happening in Coq, in particular commenting through the projects mentioned in Andrew Appel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” that took place in CPP’22 which is colocated with POPL and towards the end we also talk about agda, idris and Kind.
Links
- Nitin Twitter @NitinJohnRaj2
- Eric Twitter @EricBond10
- Appel's CPP Talk
- Proof Assistants Stack Exchange
- Coq Community
- Leo de Moura Interview