Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#15 Coq Projects, Agda, Idris, Kind

Nitin and Eric

Apr 11th 2024   |  78 min
0:00
0:00

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