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