Share
Hanselminutes is Fresh Air for Developers. A weekly commute-time podcast that promotes fresh technology and fresh voices. Talk and Tech for Developers, Life-long Learners, and Technologists.
…
continue reading
Manage episode 486880225 series 2951423
Content provided by Pedro Abreu. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Pedro Abreu or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://staging.podcastplayer.com/legal.
In this episode we talk with Nicolas Tabareau, the Head of Gallinette, one of the main teams which develop the Rocq theorem Prover at Inria.
The original idea of this interview is to talk about the rebranding from Coq into Rocq, which is very exciting to our community. However, Nicolas has such a prolific research career that I couldn’t miss the opportunity to get him to talk so much more about it.
So in this conversation we talk about his early publications in neuroscience, his views on Category Theory applied to Type Theory, Rocq’s rebranding, and the institution around it, MetaRocq and the conceptual boundaries of certifying a theory inside itself. Of course we wouldn’t miss the opportunity to also discuss how Rocq view the growing influence that Lean is gaining in our community.
Links
97 episodes
))
