#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

from Type Theory Forall · host Pedro Abreu

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

Episode metadata supplied by the publisher feed · Published Mar 27, 2022

Embed this episode

Attribution link and audio player

NOW PLAYING

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

0:00 1:17:36

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 17 minutes long.

When was this Type Theory Forall episode published?

This episode was published on March 27, 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!