Type Theory Forall

Talia Ringer is an Assistant Professor at University of Illinois Urbana-Champaign. She did her PhD at University of Washington with her thesis on Proof Repair. She’s very active on twitter @taliaringer . And in this episode we will talk about her transition from PhD to Professor, her work on diversity, her ADHD and how it has affected her career so far, and we also touch on the delicate topic of s...

In this episode we have talk with Alejandro Serrano Mena, he works on 47 degrees and is a published author of two books about Haskell: The Book of Monads and Practical Haskell. We talk about many interesting features behind functional programming such as adts, pattern matching, impredicativity, monads, effects, hacking the ghc and how all this comes together to grab industry attention to adopt fun...

In this episode we host a discussion between Anupam Das and Thorsten Altenkirch on the role of constructivism in mathematics, logic and computer science. Anupam is a lecturer in the University of Birmingham in the UK, and Thorsten Altenkirch is a CS Professor at the University of Nottingham. We discuss why constructive content in proofs matters, the law of excluded middle, the axiom of choice, cat...

In this episode I have a nice conversation with Chris Jenkins to talk about the Cedille theorem prover, based on a very concise type theory called CDLE. The main selling point of Cedille is that the theory is so small that the typing rules fit one page. And yet it is strong enough to do relevant theorem proving. This is probably the most technical episode so far. Links Leroy Jenkins Cedille Cast T...

In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some time hacking on its internals. Me and Daniel also talk about Mizar, Isar, the seL4, and how it is formalized. Torwards the end of the episode we also talk a little about his current work on the binary analysis of Aarch32 Arm Archtecture at Galois.

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 inte...

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 a...

In this episode we host Eric Bond to go through some real cool projects happening in the PL World and some of the companies behind them. We discuss some technical differences between the major interactive theorem provers out there, some of their most popular projects, and a few companies that work in the realm. Eric Bond works at 47 degrees , a consulting company on Functional Programming Language...

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 att...

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:/...

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