Type Theory Forall

#30 Actors, GADTs and Burnout - Dan and Pedro

Type Theory Forall

In this episode we have over Dan Plyukhin, a PhD Candidate from the University of Illinois Urbana-Champaign.

We talk about Dan’s research is in the field of parallelism, more specifically garbage collection in the presence of actors.

Then we also talk about Pedro’s research on translating GADTs from OCaml to Coq, and the burnout process that lead him to take 10 months off from his PhD to be with his family back in Brazil.

Links

Next Episodes


Type Theory Forall

#28 Formally Verifying Smart Contracts - Pruvendo @ Type Theory Forall

πŸ“† 2023-02-15 15:00 / βŒ› 01:10:40


Type Theory Forall

#27 Formalizing an OS: The seL4 - Gerwin Klein @ Type Theory Forall

πŸ“† 2023-02-04 21:45 / βŒ› 01:58:40


Type Theory Forall

#26 Mechanizing Modern Mathematics - Kevin Buzzard @ Type Theory Forall

πŸ“† 2023-01-16 19:30 / βŒ› 02:15:31


Type Theory Forall

#25 Formally Verifying the Tezos Codebase - Formal Land @ Type Theory Forall

πŸ“† 2022-11-21 15:05 / βŒ› 01:01:32