Type Theory Forall

#32 TyDe Systems - Jan de Muijnck-Hughes


Listen Later

In this episode we continue our conversation with Jan de Muijnck-Hughes a

Research Associate at Glasgow University. He works using all sorts of fancy
type systems mostly targeted for hardware specification, particularly with
the aid of the theorem prover Idris. This episode we start by talking a
little about Impostor Syndrome in academia and how he has learned to cope
with it and then we dive deeper into the technicalities of his research, in
particular his philosophy on Type Directed Design of Systems. We talk about
Session Types, Graded Types, Quantitative types, etc.

Don't forget to join our new discord channel!

If you like our show please consider donating any amount at ko-fi.

Links
  • Jan's website
  • Jan's twitter
  • Jan's mastodon
  • Writing and Speaking with Style
  • Artifact Eval
  • Andrej Bauer: Formalising Invisible Mathematics
  • Hedy language (Felienne Hermans)
  • Hermans' Inaugural Lecture on making PL human and inclusive
  • Epistemic Injustice
  • Richard Eisenberg interview
  • 'Software Foundations' but in Agda
  • 'System F for Fun & Profit'
  • Reviewing
  • Project Pages
    • https://dsbd-appcontrol.github.io/
    • https://border-patrol.github.io/
    • Cool People
      • Rachit Nigam
      • Clement Pit-Claudel
      • Software
        • Idris Language
        • Biblio
        • ...more
          View all episodesView all episodes
          Download on the App Store

          Type Theory ForallBy Pedro Abreu

          • 5
          • 5
          • 5
          • 5
          • 5

          5

          10 ratings


          More shows like Type Theory Forall

          View all
          In Our Time by BBC Radio 4

          In Our Time

          5,389 Listeners

          The Changelog: Software Development, Open Source by Changelog Media

          The Changelog: Software Development, Open Source

          284 Listeners

          Philosophize This! by Stephen West

          Philosophize This!

          15,093 Listeners

          The Quanta Podcast by Quanta Magazine

          The Quanta Podcast

          500 Listeners

          CoRecursive: Coding Stories by Adam Gordon Bell - Software Developer

          CoRecursive: Coding Stories

          189 Listeners

          Iowa Type Theory Commute by Aaron Stump

          Iowa Type Theory Commute

          17 Listeners

          The Real Python Podcast by Real Python

          The Real Python Podcast

          139 Listeners

          Theories of Everything with Curt Jaimungal by Theories of Everything

          Theories of Everything with Curt Jaimungal

          470 Listeners

          The Rest Is History by Goalhanger

          The Rest Is History

          13,053 Listeners

          The Haskell Interlude by Haskell Podcast

          The Haskell Interlude

          13 Listeners

          The Joy of Why by Steven Strogatz, Janna Levin and Quanta Magazine

          The Joy of Why

          502 Listeners

          The Rest Is Politics by Goalhanger

          The Rest Is Politics

          3,286 Listeners

          Oxide and Friends by Oxide Computer Company

          Oxide and Friends

          47 Listeners

          The Rest Is Politics: Leading by Goalhanger

          The Rest Is Politics: Leading

          989 Listeners

          Latent Space: The AI Engineer Podcast by swyx + Alessio

          Latent Space: The AI Engineer Podcast

          75 Listeners