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 Dan’s Personal Website Twitter: @dplyukhn

Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where he teaches engineers to write better code! In this interview we talk about how to make better code, how the knowledge of computer science theory and programming languages can help engineers to achieve that, and much more! Links Jimmy’s Personal Website Jimmy’s Twitter Mirdin’s Website Jimmy’s Blog Lastest blog post One CFG-Generator to Rule Them All Automatically Deriving Control-Flow Graph Generators from Operational Semantics Thiel Fellowship Newsletters discussed in the show Mirdin’s Newsletter Hillel Wayne’s Newsletter Eric Normand’s Newsletter Jeremy Kun’s Newsletter

In this episode we host another company that does formal method in the context of the Everscale Blockchain, and Solidity smart contracts. How and why they use formal methods in this context? Who are their clients? What are the caveats? Links Pruvendo’s Website Pruvendo’s Linkdin Pruvendo’s Twitter

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine. Links Gerwin’s Twitter Gerwin’s Website ProofCraft’s Website

Kevin Buzzard has been very passionate spreading the word among mathematicians to use theorem provers mechanize theorems of modern mathematics. In this conversation we will talk about his vision in teaching undergrads to use the Lean theorem prover, what is the Xena Project, his view of how theorem provers can change the way we do mathematics, and much more! Links Xena’s Project Twitter Xena Project’s Website Lean’s Website

In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the past developing new features to their source-to-source compiler CoqOfOcaml. In this episode we talk about their work with Tezos and how their techniques are applicable to other codebases as well! For this we talk with Formal Land founder Guillaume Claret and the proof engineers Daniel Hilst and Pierre Vial. Links Formal Land Website Formal Land Email: [email protected] Formal Land Twitter: @LandFooBar CoqOfOcaml The DAO hack

In this episode we interview Lawrence Paulson, one of the creating fathers of Isabelle. We talk about the development process, how it drew inspirations and ideas from LCF and Boyer Moore. What tools were used, it’s strenghts and weaknesses, and all about the historical context at the time! We also briefly talk about his formalization of the Gödel’s Incompletenes theorems in Isabelle Paulson have quite an extensive CV, he is a professor at Cambridge, have published more than 100 papers, is an ACM fellow since 2008, is a member of the royal society since 2017, among many other things! Links Larry’s Website Larry’s Twitter Larry’s Blog

In this episode we talk about Sigplan, the organization behind the most important conferences and proceedings in our field. What is the SIGPLAN? What exactly does it do? How is it organized? How are things published? To answer these and many other questions we talk with Jens Palsberg, a professor at UCLA, who is the past chair of the SIGPLAN. And also Jonathan Aldrich, a professor at the CMU, who is a member of the ACM publication board. Links Jen’s Website Jonathan’s Website Jonathan’s Twitter Sigplan Blog Post on Hybrid Conferences SIGPlAN-M Mentoring Program

In this episode Cody Roux teaches some interesting concepts that people care about in Mathematics and Logic as a way to try to understand what is going on in the universe around us! In particular we will try to explain concepts such as Impredicativity, Excluded Middle, Group Theory, Model Theory, Kripke Models, Realizability, The Markov Principle, Cut Elimination, and other stuff! Links Cody’s website Cody’s dblp

In this episode Conal Elliott gives a more concrete presentation on what is Denotational Design is and how to use it in practice. It is a continuation of episode #17, in which we had an in-depth philosophical conversation to explain why he believes that Denotational Design is a superior form of reasoning in the realm of computer science. We also continue a discussion raised by Dan Ghica on the last episode on the need for Operational Semantics and the role of elegance in reasoning and design. Along the way we also address the questions sent by the listeners in these last episodes. Links Conal’s website Play/work with Conal Conal’s twitter: @conal The simple essence of automatic differentiation Compiling to categories Generic parallel functional programming Denotational design with type class morphisms Quotes “A theory appears beautiful or elegant […] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons.” - Murray Gell-Mann, Beauty and Elegance in Physics. “In Galileo’s time, professors of philosophy and theology—the subjects were inseparable—produced grand discourses on the nature of reality, the structure of the universe, and the way the world works, all based on sophisticated metaphysical arguments. Meanwhile, Galileo measured how fast balls roll down inclined planes. How mundane! But the learned discourses, while grand, were vague. Galileo’s investigations were clear and precise. The old metaphysics never progressed, while Galileo’s work bore abundant, and at length spectacular, fruit. Galileo too cared about the big questions, but he realized that getting genuine answers requires patience and humility before the facts.” - Frank Wilczek, (The Lightness of Being: Mass, Ether, and the Unification of Forces) “We must make here a clear distinction between belief and faith, because, in general practice, belief has come to mean a state of mind which is almost the opposite of faith. Belief, as I use the word here, is the insistence that the truth is what one would ‘lief’ or wish it to be. The believer will open his mind to the truth on the condition that it fits in with his preconceived ideas and wishes. Faith, on the other hand, is an unreserved opening of the mind to the truth, whatever it may turn out to be. Faith has no preconceptions; it is a plunge into the unknown. Belief clings, but faith lets go. In this sense of the word, faith is the essential virtue of science, and likewise of any religion that is not self-deception.” - Alan Watts (The Wisdom of Insecurity: A Message for an Age of Anxiety)