Эпизоды
-
In this episode we talk with Guannan Wei, from Purdue University. Guannanfinished his PhD last year under Tiark Rompf, and is currently doing hisPost-Doc with Tiark. Guannan has worked on a plethora of differentcompilers topics, and in this conversation we will talk about Staging,Futamura Projections, Symbolic Execution, Compiler Applications in SmartContracts and Quantum Programming. Towards the end of the episode we alsotalk about his application experiences for the position of a Professorship inthe US an a few other contries.
Guannan’s Website @guannanwei on X -
In this episode we celebrate 3 years of existence of this podcast byreflecting on the journey so far, what is my philosophy, how do Iapproach the interviews, my overall goals for the show, and some of our plansfor the future.
In order to achieve this, I first take a detour and tell you a little moreabout my personal history, and my carreer in type theory and programminglanguages.
-
Пропущенные эпизоды?
-
In this episode we talk with Eduardo Rafael. He isself-thaught programming languages enthusiast, youtuber, twitch streamer,multi-skilled programmer that has worked in different aspects of computerscience such as PL, operating systems, blockchain, and many other stuff. Inthis conversation we talk about his experience as a developer and hacker thatdidn’t follow the conventional paths of going to school and what are thestrategies to navigate the vast ocean of knowledge without guidance ofteachers 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 worksunder Aaron Stump and has been working on revamping the theorem proverCedille 2. In this episode we tackle fundamental questions about thefoundations of the theorem provers, Cedille and Cedille 2.
Links Andrew’s Website AndrasKovacs’ Smalltt Failure of Normalization in Impredicative Type Theory withProof-Irrelevant Propositional Equality Impredicative Encodings of (Higher) Inductive Types -
Not satisfied with implementing one of the most popular automated theoremprovers, Z3, Leo de Moura also tackles another extremely hard problem inour field and implements a brand new interactivetheorem prover from scratch, Lean. In this episode we dive into the mind andphilosophy 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 aResearch Associate at Glasgow University. He works using all sorts of fancytype systems mostly targeted for hardware specification, particularly withthe aid of the theorem prover Idris. This episode we start by talking alittle about Impostor Syndrome in academia and how he has learned to copewith it and then we dive deeper into the technicalities of his research, inparticular his philosophy on Type Directed Design of Systems. We talk aboutSession 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’ ReviewingProject Pages https://dsbd-appcontrol.github.io/ https://border-patrol.github.io/Cool People Rachit Nigam Clement Pit-ClaudelSoftware Idris Language Biblio -
In this episode we have a deep conversation with Jan de Muijnck-Hughes, talksabout all the cool research he has done with idris, hardware and different kindsof interesting type systems such as session types, quantitative types and gradedtypes. In the second half we discuss all the different kinds of problems thathas been going on in PL academia lately and what we can do as a community toaddress 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 DelftLinks 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’ ReviewingProject Pages https://dsbd-appcontrol.github.io/ https://border-patrol.github.io/Cool People Rachit Nigam Clement Pit-ClaudelSoftware Idris Language Biblio -
In this episode we have over Dan Plyukhin, a PhD Candidate fromthe University of Illinois Urbana-Champaign.
We talk about Dan’s research is in the field of parallelism, morespecifically 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 tobe 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 heteaches engineers to write better code! In this interview we talk about howto make better code, how the knowledge of computer science theory andprogramming 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 FellowshipNewsletters 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 thecontext 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 themicrokernel seL4 which was done using Isabelle atNICTA / Data61 in Australia. We also talk a little about his PhD Projectveryfing 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 amongmathematicians to use theorem provers mechanize theorems of modernmathematics. In this conversation we will talk about his vision in teachingundergrads to use the Lean theorem prover, what is the Xena Project, his viewof 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 formallyverifying the Tezos codebase! I have worked with them in the past developingnew features to their source-to-source compiler CoqOfOcaml. In this episode wetalk about their work with Tezos and how their techniques are applicable toother codebases as well! For this we talk with Formal Land founderGuillaume 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 ofIsabelle.
We talk about the development process, how it drew inspirations andideas from LCF and Boyer Moore. What tools were used, it’s strenghts andweaknesses, and all about the historical context at the time! We also brieflytalk about his formalization of the Gödel’s Incompletenes theorems in Isabelle
Paulson have quite an extensive CV, he is a professor at Cambridge, havepublished more than 100 papers, is an ACM fellow since 2008, is a member ofthe 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 mostimportant conferences and proceedings in our field. What is the SIGPLAN? Whatexactly does it do? How is it organized? How are things published? To answerthese and many other questions we talk with Jens Palsberg, a professor atUCLA, who is the past chair of the SIGPLAN. And also Jonathan Aldrich, aprofessor 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 careabout in Mathematics and Logic as a way to try to understand what is going onin the universe around us! In particular we will try to explain concepts suchas Impredicativity, Excluded Middle, Group Theory, Model Theory, KripkeModels, Realizability, The Markov Principle, Cut Elimination, and otherstuff!
Links Cody’s website Cody’s dblp -
In this episode Conal Elliott gives a more concrete presentationon 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 philosophicalconversation to explain why he believes thatDenotational Design is a superior form of reasoning in the realm of computerscience.
We also continue a discussion raised by Dan Ghica on the last episode on theneed for Operational Semantics and the role of elegance in reasoning anddesign.
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 morphismsQuotes“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 ProgrammingLanguage Research Lab of the Huaweii Research Centre Edinburgh. We talk about his work on both institutions, which includes topics such asCategory Theory, String Diagrams, and Game Semantics. We also briefly discuss the current publication process of our field andentertain some thoughts on how to make it better. Finally, we touch onmore personal topics such as his views about Elegance, making an insightfulcounterpoint to Conal’s opinions on Denotational Semantics vs. OperationalSemantics.
Links Dan’s Twitter: @danghica Dan’s Website Job advert for Huawei positionsTalks 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 lecturesPapers 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 equivalenceOther 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 SupunAbeysinghe. We will talk about their experience learning Coq and we guideourselves 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. AndSupun works more along the lines of machine learning in the context ofsystems.
-
In this episode Cody Roux talks about the Gödel’s Incompleteness Theorems. We gothrough it’s underlying historical context, Hilbert’s Program, how it relateswith 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 - Показать больше