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

          • 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,133 Listeners

          Iowa Type Theory Commute by Aaron Stump

          Iowa Type Theory Commute

          17 Listeners

          Dwarkesh Podcast by Dwarkesh Patel

          Dwarkesh Podcast

          455 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,329 Listeners

          Oxide and Friends by Oxide Computer Company

          Oxide and Friends

          59 Listeners

          The Rest Is Money by Goalhanger

          The Rest Is Money

          186 Listeners

          BG2Pod with Brad Gerstner and Bill Gurley by BG2Pod

          BG2Pod with Brad Gerstner and Bill Gurley

          485 Listeners