#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric
Type Theory Forall
English - March 27, 2022 15:15 - 1 hour - 61.5 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #14 POPL, Parametricity, Scala, DOT - Nitin and Eric
Next Episode: #16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx
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