![Type Theory Forall artwork](https://is5-ssl.mzstatic.com/image/thumb/Podcasts124/v4/ed/de/43/edde43db-febe-b892-3a30-358ebe2e2c07/mza_16532267942080647912.png/100x100bb.jpg)
#32 TyDe Systems - Jan de Muijnck-Hughes
Type Theory Forall
English - July 22, 2023 15:50 - 1 hour - 82.6 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
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