DiscoverType Theory Forall
Claim Ownership
42 Episodes
Reverse
In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer.
He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris.
In today’s episode we talk about the story behind writing The Little Typer together with Dan Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.
Some links:
David's Website
David's X
Lean Zulip Chat
Truth of a proposition, evidence of a judgement, validity of a proof
In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer.
He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris.
David is a super upbeat person and I feel that we could spend hundreds of hours talking about Functional Programming Writing and Dependent Types, and we still wouldn’t run out of topics!
In this episode we talk with Guannan Wei, from Purdue University. Guannan
finished his PhD last year under Tiark Rompf, and is currently doing his
Post-Doc with Tiark. Guannan has worked on a plethora of different
compilers topics, and in this conversation we will talk about Staging,
Futamura Projections, Symbolic Execution, Compiler Applications in Smart
Contracts and Quantum Programming. Towards the end of the episode we also
talk about his application experiences for the position of a Professorship in
the US an a few other contries.
Guannan's Website
@guannanwei on X
In this episode we celebrate 3 years of existence of this podcast by
reflecting on the journey so far, what is my philosophy, how do I
approach the interviews, my overall goals for the show, and some of our plans
for the future.
In order to achieve this, I first take a detour and tell you a little more
about my personal history, and my carreer in type theory and programming
languages.
In this episode we talk with Eduardo Rafael. He is
self-thaught programming languages enthusiast, youtuber, twitch streamer,
multi-skilled programmer that has worked in different aspects of computer
science such as PL, operating systems, blockchain, and many other stuff. In
this conversation we talk about his experience as a developer and hacker that
didn’t follow the conventional paths of going to school and what are the
strategies to navigate the vast ocean of knowledge without guidance of
teachers or institutions.
Links
Eduardo's Twitter
Eduardo's Twitch
Eduardo's Youtube
Feynman Algorithm
Andrew Marmaduke is a PhD Candidate from the University of Iowa, he works
under Aaron Stump and has been working on revamping the theorem prover
Cedille 2. In this episode we tackle fundamental questions about the
foundations of the theorem provers, Cedille and Cedille 2.
Links
Andrew's Website
AndrasKovacs' Smalltt
Failure of Normalization in Impredicative Type Theory with
Proof-Irrelevant Propositional Equality
Impredicative Encodings of (Higher) Inductive Types
Not satisfied with implementing one of the most popular automated theorem
provers, Z3, Leo de Moura also tackles another extremely hard problem in
our field and implements a brand new interactive
theorem prover from scratch, Lean. In this episode we dive into the mind and
philosophy of this man.
Links
Leo's Website
Lean
Z3
The Church of Logic Podcast
In this episode we continue our conversation with Jan de Muijnck-Hughes a
Research Associate at Glasgow University. He works using all sorts of fancy
type systems mostly targeted for hardware specification, particularly with
the aid of the theorem prover Idris. This episode we start by talking a
little about Impostor Syndrome in academia and how he has learned to cope
with it and then we dive deeper into the technicalities of his research, in
particular his philosophy on Type Directed Design of Systems. We talk about
Session Types, Graded Types, Quantitative types, etc.
Don't forget to join our new discord channel!
If you like our show please consider donating any amount at ko-fi.
Links
Jan's website
Jan's twitter
Jan's mastodon
Writing and Speaking with Style
Artifact Eval
Andrej Bauer: Formalising Invisible Mathematics
Hedy language (Felienne Hermans)
Hermans' Inaugural Lecture on making PL human and inclusive
Epistemic Injustice
Richard Eisenberg interview
'Software Foundations' but in Agda
'System F for Fun & Profit'
Reviewing
Project Pages
https://dsbd-appcontrol.github.io/
https://border-patrol.github.io/
Cool People
Rachit Nigam
Clement Pit-Claudel
Software
Idris Language
Biblio
In this episode we have a deep conversation with Jan de Muijnck-Hughes, talks
about all the cool research he has done with idris, hardware and different kinds
of interesting type systems such as session types, quantitative types and graded
types. In the second half we discuss all the different kinds of problems that
has been going on in PL academia lately and what we can do as a community to
address those issues.
Also, we have a discord channel now, join us!
If you like our show please consider donating any amount at ko-fi.
Errata:
Jan mentions 'Jeff Foster' when, in fact, he meant Nate Foster
This is the SIGCOMM 'Call': https://sigcomm.quest/
Felinne Hermans did her PhD at Eindhoven and not Delft
Links
Jan's website
Jan's twitter
Jan's mastodon
Writing and Speaking with Style
Artifact Eval
Andrej Bauer: Formalising Invisible Mathematics
Hedy language (Felienne Hermans)
Hermans' Inaugural Lecture on making PL human and inclusive
Epistemic Injustice
Richard Eisenberg interview
'Software Foundations' but in Agda
'System F for Fun & Profit'
Reviewing
Project Pages
https://dsbd-appcontrol.github.io/
https://border-patrol.github.io/
Cool People
Rachit Nigam
Clement Pit-Claudel
Software
Idris Language
Biblio
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: contact@formal.land
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
Comments
United States