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)

In this episode, me and Eric Bond have a great conversation with Dan R. Ghica, a professor at Birmingham University and Director of the Programming Language Research Lab of the Huaweii Research Centre Edinburgh. We talk about his work on both institutions, which includes topics such as Category Theory, String Diagrams, and Game Semantics. We also briefly discuss the current publication process of our field and entertain some thoughts on how to make it better. Finally, we touch on more personal topics such as his views about Elegance, making an insightful counterpoint to Conal’s opinions on Denotational Semantics vs. Operational Semantics.

Links

• Dan's Twitter: @danghica
• Dan's Website
• Job advert for Huawei positions

Talks and Lectures

• Dan's talk on Syntactic Trinitarianism (terms, graphs, diagrams)
• Dan's talk on a similar, more semantics-oriented talk at TERMGRAPH
• Dan's OPLSS course on (denotational) game semantics
• Game semantics lectures

Papers

• Paper on string diagrams and their applications to reverse automatic differentiation (long paper, part of it to appear in FSCD 2020)
• Paper on automatic differentiation and string diagrams
• Paper on effect handlers
• Paper on optimisation with constructive reals
• Paper on digital circuits and string diagrams
• Paper on functorial boxes for string diagrams
• A Game semantics paper mentioned during the conversation
• Decidability via game semantics
• Landmark paper on undecidability of observational equivalence

Other Links

• Penrose book
• Book on type-level string diagrams
• Proof assistant for higher categories
• The Programming Journal
• Midlands Graduate School

In today’s episode I invite two friends of mine Patrick Lafontaine and Supun Abeysinghe. We will talk about their experience learning Coq and we guide ourselves in a survey that I gave all the 83 students in the class. The class was thought by my advisor Benjamin Delaware and I was his TA.

Patrick researches compilers and have done work in particular with Rust. And Supun works more along the lines of machine learning in the context of systems.

In this episode Cody Roux talks about the Gödel's Incompleteness Theorems. We go through it’s underlying historical context, Hilbert’s Program, how it relates with Turing, Church, Von Neumann, Termination and more.

Links

• Cody's website
• Cody's dblp
• The Lady or the Tiger? - Short Story
• The Lady or the Tiger? - Amazon
• Logicomix
• An Introduction to Gödel's Theorems
• Jeremy Avigad's Lecture Notes

In this episode I had the pleasure to have an in-depth conversation with Conal Elliott about his life, his work, his philosophy and his many opinions about research and the current state of PL Research and how it lead him to come with the concept of Denotational Design. Conal got his PhD at CMU in the 90s under Frank Pfenning working on Higher-Order Unification, after that he has devoted his life on thinking and refining graphic computation and the tools behind it.

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
• Functional Images
• Functional Reactive Animation
• Alphabet Versus the Goddess - Leonard Shlain
• The information - James Gleick
• Murray Gell-Mann’s definition of beauty/elegance: "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."
• A John Backus quote (from his Turing Award lecture): “Many creative computer scientists have retreated from inventing languages to inventing tools for describing them. Unfortunately, they have been largely content to apply their elegant new tools to studying the warts and moles of existing languages. After examining the appalling type structure of conventional languages, using the elegant tools developed by Dana Scott, it is surprising that so many of us remain passively content with that structure instead of energetically searching for new ones.”

In this episode we interview Jesper Cockx, one of the core developers on Agda. We talk about the philosophy behind Agda, his work on pattern matching, the Uniqueness of Identity of Proofs, UIP for short, and why it is inconsistent with Homotopy Type Theory.

Links

• Jesper's Website
• Jesper's Twitter: @agdakx
• Jesper's PhD Thesis
• Rewrite Theory paper
• Pattern matching without K paper (Check his website for more)
• EuroProofNet
• WITS Talks on Youtube (Workshop on the Implementation of Type Systems)
• Agda Zulip
• Agda Mailing List
• Ataca Github
• Wadler's book on Agda
• Stump's book on Agda

In this episode me, Eric and Nitin continues our conversation started in the last episode. This time we move our attention to the cool projects happening in Coq, in particular commenting through the projects mentioned in Andrew Appel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” that took place in CPP’22 which is colocated with POPL and towards the end we also talk about agda, idris and Kind.

Links

• Nitin Twitter @NitinJohnRaj2
• Eric Twitter @EricBond10
• Appel's CPP Talk
• Proof Assistants Stack Exchange
• Coq Community
• Leo de Moura Interview

In this episode I gather with two good friends Eric and Nitin to randomly talk random subjects that pops up. Among them we talked about POPL, Scala, Isabelle, Parametricity, Dependent Object Types (DOT, for short) and more!

Links

• Nitin Twitter @NitinJohnRaj2
• Eric Twitter @EricBond10
• Collection of links on logical relations
• Theorems for Free
• Reynolds Paper
• Practical Foundations for Programming Languages

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: [email protected]
• 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: [email protected]

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

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 Languages, specially on Scala and Haskell. You can find Eric @ericbond10 on Twitter.

During the episode we mention PL Talks and the Midlands Graduate School in the Foundations of Computing Science 2021.

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