Type Theory Forall

In this episode we interview Zeina Migeed, a PhD Student at University of California Los Angeles, advised by Prof. Jens Palsberg She Researches Gradual Types and had a paper published at POPL'20 named "What is Decidable about Gradual Types". here is a link to it As the name of the episode suggests, I'll be asking her all the dumb questions related to not only gradual types, but also intersection types and recursive types as well!

In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept. Links: Yves email: yves.bertot@inria.fr Affichage et manipulation interactive de formules mathématiques dans les documents structurés - Check figure 15 for an example on how Yves’ tools would build trees internally A video showing his tool in practice, doing proofs with mouse clicks A Genereic Approach to Building User Interfaces for Theorem Provers

Eric Bond works at 47 degrees, a consulting firm specializing in Functional Programming. He shares insights into the rise of Lean in formal verification and the challenges of Haskell, contrasting it with Isabelle and Coq. The conversation highlights innovations in functional programming and type theory, especially in the context of the pandemic, promoting best practices in consulting. Eric also discusses the growing relevance of formal verification in the cryptocurrency space, alongside the enriching contributions of programming communities.

In this episode we host Dan Zheng, an alumni of Purdue University that now works at Google at real cool projects that relates ML and PL. We chat about how was his transition from undergrad to such a huge company like Google. We talk about cool languages such as Lantern, LLVM, LMS, Julia, Rust, Racket, Scala. How does ML and PL can be used to enhance each other. And towards the end we shift our attention to mental health, both in the academia and in the industry. You can find Dan at twitter @dancherp

In this episode we host Rajan Walia and John Sarracino. Rajan is a last year PhD Student from Indiana University, working under Sam Tobin-Hochstadt. And John is a Postdoc working with Greg Morriset at Cornell University. We talk about Grad School life, how academia life looks like, pressure to publish, work-life balance, industry vs academia, and much more! Here you can find John’s Website. http://goto.ucsd.edu/~john/ And here is Matt Might’s website mentioned in the episode. http://matt.might.net/#blog

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research: What is PL research? Why does it matter? Why is it cool? What is Lambda Calculus? What is Type Theory? Church-Turing Thesis? Curry-Howard Correspondence? What are proof assistants? Why are they cool? Don’t forget to follow Ben on twitter @GhostofBendy

Who is Pedro Abreu? What is the goal of this Podcast? What are My Research Interests? In this episode I share about my internship experiences at Nicta (data61 now), Sifive, Galois and Nomadic Labs. Welcome! Don’t forget to checkout Galois’ new podcast hosted by Joey Dodds and Shpat Morina. Click Here