Type Theory Forall

This episode is about the journey of a programmer that converted himself into a Haskell developer after working with C/C++ for more than 10years. Here are a few questions that you'll find the answer to in this episode: What does he find so compelling about Haskell? Why did it make him dive deeper into the Theoretical Computer Science? Why did it make him learn Coq and Category Theory? How does Coq compare with ACL2? How do both Coq and ACL2 compares to TLA+? Did learning Coq make John a better programmer? Links John's Email: johnw@newartisans.com John's Twitter: @jwiegley

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 sexism in academia. Links Talia's Twitter Sigplan Mentoring TIL: a type-directed, optimizing compiler for ML Neuro Divergent in CS Neuro Divergent in CS - Slack Overblur

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 functional programming features over the past decade. Links Our new twitter @ttforall Alejandro's twitter Book of Monads Practical Haskell The Haskell Interlude Tweag's youtube channel on the GHC

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, category theory, and much more! Links Thorsten's website Anupam's website Thorsten's Book on Python The Proof Theory Blog High School Algebra Stanford Encyclopedia of Philosophy

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 The Iowa Type Theory Commute Cedille Page Github Page

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