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

Twitter Mentions