Artwork

Content provided by Pedro Abreu. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Pedro Abreu or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.
Player FM - Podcast App
Go offline with the Player FM app!

#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra

2:06:47
 
Share
 

Manage episode 482748257 series 2951423
Content provided by Pedro Abreu. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Pedro Abreu or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.

Wouter Swierstra is a Math Bachelor’s from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Nottingham, did a post-doc at Chalmers, has experience in the industry working on facilitating the design of embedded system using FP and currently is a Professor at the University of Utrecht and co-host of the Haskell Interlude Podcast.

In this episode we talk about his trajectory into formal methods and functional programming. We talk about Datatypes a la Carte, the Expression Problem, Functional Pearls, Program Synthesis vs Program Calculation, and much more!

0:00 – Intro & Welcome 0:02:08 – Announcing the Type Theory Forall Merch Store! 1:12 – Early Influences: From Lenses to Logic 4:40 – Discovering Functional Programming in Utrecht 8:15 – On Monads, Papers, and Learning by Teaching 12:20 – What Makes a Paper ‘Beautiful’? 17:50 – PhD in Nottingham: Theory Meets Community 22:00 – Writing ‘Certified Programming with Dependent Types’ 29:10 – Teaching Dependent Types: Challenges and Joys 34:00 – On Agda vs Coq: Philosophies and Use Cases 38:40 – Type-Driven Development in Practice 45:05 – The Power of Elegant Proofs 52:00 – Advice to Aspiring Researchers in Type Theory 1:03:00 – Beating C with Functional Programming 1:20:00 – Formal Verification and Loop Invariants 1:33:28 – Program Calculation vs Program Synthesis 1:39:00 – Formalizing Blockchain 2:01:38 – Final Thoughts

Links

Discount code for 10% off: typetheory

  continue reading

90 episodes

Artwork
iconShare
 
Manage episode 482748257 series 2951423
Content provided by Pedro Abreu. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Pedro Abreu or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.

Wouter Swierstra is a Math Bachelor’s from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Nottingham, did a post-doc at Chalmers, has experience in the industry working on facilitating the design of embedded system using FP and currently is a Professor at the University of Utrecht and co-host of the Haskell Interlude Podcast.

In this episode we talk about his trajectory into formal methods and functional programming. We talk about Datatypes a la Carte, the Expression Problem, Functional Pearls, Program Synthesis vs Program Calculation, and much more!

0:00 – Intro & Welcome 0:02:08 – Announcing the Type Theory Forall Merch Store! 1:12 – Early Influences: From Lenses to Logic 4:40 – Discovering Functional Programming in Utrecht 8:15 – On Monads, Papers, and Learning by Teaching 12:20 – What Makes a Paper ‘Beautiful’? 17:50 – PhD in Nottingham: Theory Meets Community 22:00 – Writing ‘Certified Programming with Dependent Types’ 29:10 – Teaching Dependent Types: Challenges and Joys 34:00 – On Agda vs Coq: Philosophies and Use Cases 38:40 – Type-Driven Development in Practice 45:05 – The Power of Elegant Proofs 52:00 – Advice to Aspiring Researchers in Type Theory 1:03:00 – Beating C with Functional Programming 1:20:00 – Formal Verification and Loop Invariants 1:33:28 – Program Calculation vs Program Synthesis 1:39:00 – Formalizing Blockchain 2:01:38 – Final Thoughts

Links

Discount code for 10% off: typetheory

  continue reading

90 episodes

All episodes

×
 
Loading …

Welcome to Player FM!

Player FM is scanning the web for high-quality podcasts for you to enjoy right now. It's the best podcast app and works on Android, iPhone, and the web. Signup to sync subscriptions across devices.

 

Quick Reference Guide

Copyright 2025 | Privacy Policy | Terms of Service | | Copyright
Listen to this show while you explore
Play