Radio and PodcastLive Radio & PodcastsOpening Radio and Podcast...
Radio and PodcastLive Radio & PodcastsFetching podcast shows and categories...
Radio and PodcastLive Radio & PodcastsFetching podcast episodes...
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
The Curry-Howard isomorphism for the law of excluded middle, as a radio drama. I first saw a version of this story performed by Phil Wadler...
I discuss a nice paper I quite enjoyed reading, called The Calculated Typer , by Garby, Bahr, and Hutton. The authors take a very nice gener...
In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CP...
In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming la...
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the nor...
I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderf...
In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some proce...
To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-boun...
In this episode, I shoot down last episode's proposal -- at least in the version I discussed -- based on an amazing observation from an...
In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating...
I correct what I said in the last episode about the author of the proof of FD from last episode based on intersection types. I also describe...
Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this...
I discuss the paper "A Direct Proof of the Finite Developments Theorem" , by Roel de Vrijer. See also the write-up at my blog.
The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and...
In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL , by Christian Urban. This paper shows how to reason with terms modu...
I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nice...
I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations , which proposes a benchmark problem for mechanizing Programm...
I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga...
In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theore...
In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing&a...
In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof...
It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STL...
Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). Bu...
I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
In this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some...
This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and...
In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean....
In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here .
DCS is a new functional programming language I am designing and implementing with Stefan Monnier . DCS has a pure, terminating core, around...
I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumpt...
I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes . Coming soon: a discussion of semantics of subtyping...
In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by all...
In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms...
In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the var...
We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemen...
In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Eq...
I continue discussing the Puject and Tabareau paper, " Observational Equality -- Now for Good ", in particular discussing more about how the...
In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier...
I pause the chapter on extensionality in type theory to talk about something very exciting that I just learned about (though the project was...
In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says...
This episode begins a new chapter on extensionality in type theory, where we seek to equate terms in different ways based on their types. Th...
In this episode, I talk about two papers from the 3rd International Workshop on Formal Methods for Blockchains , 2021. Also, I am continuing...
In this episode, I discuss this paper , "Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts", by Bernardo et al. The paper gives a...
In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart co...
I start off a new chapter (seventeen!) of the podcast, to talk about formal methods for blockchain systems. In the next few episodes, we wil...
I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data str...
I discuss separation logic, as presented in this seminal paper by the great John C. Reynolds. I did not go very far into the topic, so pleas...
In this episode, I talk briefly about Rust, which uses compile-time analysis to ensure that code is memory-safe (and also free of data races...
I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to dec...
In this episode, I start a new chapter (we are up to Chapter 16, here), about verifying safe manual management of memory. I have personally...