Type Theory Forall

#51 s/Coq/Rocq - Nicolas Tabareau


Listen Later

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
  • Type Theory Forall Store
  • Type Theory Forall Website
  • Nicolas Tabareau Website
  • MetaRocq Github
  • ...more
    View all episodesView all episodes
    Download on the App Store

    Type Theory ForallBy Pedro Abreu

    • 4.8
    • 4.8
    • 4.8
    • 4.8
    • 4.8

    4.8

    13 ratings


    More shows like Type Theory Forall

    View all
    Hanselminutes with Scott Hanselman by Scott Hanselman

    Hanselminutes with Scott Hanselman

    380 Listeners

    The Quanta Podcast by Quanta Magazine

    The Quanta Podcast

    526 Listeners

    ChinaTalk by Jordan Schneider

    ChinaTalk

    284 Listeners

    CoRecursive: Coding Stories by Adam Gordon Bell - Software Developer

    CoRecursive: Coding Stories

    188 Listeners

    Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas by Sean Carroll | Wondery

    Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas

    4,131 Listeners

    Iowa Type Theory Commute by Aaron Stump

    Iowa Type Theory Commute

    17 Listeners

    Dwarkesh Podcast by Dwarkesh Patel

    Dwarkesh Podcast

    456 Listeners

    Signals and Threads by Jane Street

    Signals and Threads

    73 Listeners

    The Haskell Interlude by Haskell Podcast

    The Haskell Interlude

    13 Listeners

    Software Unscripted by Richard Feldman

    Software Unscripted

    26 Listeners

    The Rest Is Politics by Goalhanger

    The Rest Is Politics

    3,324 Listeners

    Oxide and Friends by Oxide Computer Company

    Oxide and Friends

    59 Listeners

    The Rest Is Money by Goalhanger

    The Rest Is Money

    183 Listeners

    BG2Pod with Brad Gerstner and Bill Gurley by BG2Pod

    BG2Pod with Brad Gerstner and Bill Gurley

    483 Listeners