Player FM - Internet Radio Done Right
17 subscribers
Checked 2M ago
Added five years ago
Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.
Player FM - Podcast App
Go offline with the Player FM app!
Go offline with the Player FM app!
Podcasts Worth a Listen
SPONSORED
<
<div class="span index">1</div> <span><a class="" data-remote="true" data-type="html" href="/series/squid-game-the-official-podcast">Squid Game: The Official Podcast</a></span>


The final season is here—and Squid Game: The Official Podcast is your ultimate companion to the end of the Game. Hosts Phil Yu and Kiera Please return once more to break down every shocking twist and betrayal, and the choices that will determine who, if anyone, makes it out alive. Will Player 456 and the cast of characters we’ve grown to love finally be able to dismantle the games for good? Or will the cycle continue? Alongside creators, cultural critics, and viral internet voices, Phil and Kiera provide their own theories for how the season ends, and what Squid Game ultimately reveals about power, sacrifice, and the systems that shape us. The biggest question isn’t who wins—it’s what it means to be human. Squid Game: The Official Podcast returns Friday, June 27th.
Iowa Type Theory Commute
Mark all (un)played …
Manage series 2823367
Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
…
continue reading
175 episodes
Mark all (un)played …
Manage series 2823367
Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
…
continue reading
175 episodes
All episodes
×I
Iowa Type Theory Commute

1 Correction: the Correct Author of the Proof from Last Episode, and an AI flop 7:10
7:10
Play Later
Play Later
Lists
Like
Liked7:10
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 AI flopping when I ask it a question about this.
I
Iowa Type Theory Commute

1 Krivine's Proof of FD, Using Intersection Types 21:35
21:35
Play Later
Play Later
Lists
Like
Liked21:35
Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this episode.
I
Iowa Type Theory Commute

1 A Measure-Based Proof of Finite Developments 23:24
23:24
Play Later
Play Later
Lists
Like
Liked23:24
I discuss the paper "A Direct Proof of the Finite Developments Theorem" , by Roel de Vrijer. See also the write-up at my blog.
I
Iowa Type Theory Commute

1 Introduction to the Finite Developments Theorem 15:54
15:54
Play Later
Play Later
Lists
Like
Liked15:54
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 their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.…
I
Iowa Type Theory Commute

In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL , by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.
I
Iowa Type Theory Commute

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction. I also answer a listener's question about what "computational type theory" means. Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.…
I
Iowa Type Theory Commute

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations , which proposes a benchmark problem for mechanizing Programming Language theory.
I
Iowa Type Theory Commute

I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.
I
Iowa Type Theory Commute

1 Introduction to Formalizing Programming Languages Theory 12:20
12:20
Play Later
Play Later
Lists
Like
Liked12:20
In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.
I
Iowa Type Theory Commute

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's original proof and some historical comments.
I
Iowa Type Theory Commute

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 methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).…
I
Iowa Type Theory Commute

1 Arithmetic operations in simply typed lambda calculus 9:56
9:56
Play Later
Play Later
Lists
Like
Liked9:56
It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A. Interestingly, things change with exponentiation, which we will consider in the next episode.…
I
Iowa Type Theory Commute

1 The curious case of exponentiation in simply typed lambda calculus 7:29
7:29
Play Later
Play Later
Lists
Like
Liked7:29
Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surprisingly, the type is non-uniform. If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A. The second argument needs to have type at strictly higher order than the first argument. This has the fascinating consequence that we cannot define self-exponentiation, \ x . exp x x. That term would reduce to \ x . x x, which is provably not typable in STLC.…
I
Iowa Type Theory Commute

I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
I
Iowa Type Theory Commute

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 basic examples. Subsequent episodes will discuss various interesting nuances...
I
Iowa Type Theory Commute

This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.…
I
Iowa Type Theory Commute

1 DCS compared to termination checkers for type theories 19:45
19:45
Play Later
Play Later
Lists
Like
Liked19:45
In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here .
I
Iowa Type Theory Commute

In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here .
I
Iowa Type Theory Commute

DCS is a new functional programming language I am designing and implementing with Stefan Monnier . DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation. In this episode, I talk about this basic design, and its rationale.
I
Iowa Type Theory Commute

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping. With coercive subtyping, we have subtyping axioms "A <: B by c", where c is a function from A to B. The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be converted to one of type B. Subsumptive subtyping says that A <: B means that the meaning of A is a subset of the meaning of B. So this kind of subtyping depends on a semantics for types. A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants. So a type like Integer might be interpreted as the set of all integers, etc. Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms. For in that situation, A <: B does not imply List A <: List B, because Nil A is an inhabitant of List A but not of List B (which requires instead Nil B). Join the telegram group here .…
I
Iowa Type Theory Commute

I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes . Coming soon: a discussion of semantics of subtyping.
I
Iowa Type Theory Commute

In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make types work out. Examples are lifting functions with monad transformers, or even just the pure/return functions for applicative functors/monads.…
I
Iowa Type Theory Commute

In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus. I mostly focus here on how subtype constraints allow typing any term (which seems surprising). You can join the telegram group for discussion related to the podcast.…
In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.
I
Iowa Type Theory Commute

We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code. I also talk about how subtyping could help realize a new vision for practical strong functional programming, where the language has a pure, terminating core language, then a monad for pure but possibly diverging computation, and finally a monad for impurity and divergence.…
I
Iowa Type Theory Commute

1 Last episode discussing Observational Equality Now for Good 12:15
12:15
Play Later
Play Later
Lists
Like
Liked12:15
In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion. See this paper by Peter Dybjer for more about that feature. Also, feel free to join the new Telegram group for the podcast if you want to discuss episodes.…
I
Iowa Type Theory Commute

I continue discussing the Puject and Tabareau paper, " Observational Equality -- Now for Good ", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to cast terms from one type to another. Also, in exciting news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes. I will be monitoring the group. I believe you have to request to join, and then I approve (it might take me until later in the day to do that, just fyi). The invitation link is here .…
I
Iowa Type Theory Commute

In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier work of McBride, Swierstra, and Altenkirch (which I will cover in a later episode) on a new approach to making a type theory extensional. The idea is to have equality types reduce, within the theory, to statements of extensional equality for the type of the values being equated.…
I
Iowa Type Theory Commute

I pause the chapter on extensionality in type theory to talk about something very exciting that I just learned about (though the project was completed Summer 2022): the so-called Liquid Tensor Experiment , to formalize a recent very difficult proof by a mathematician named Peter Scholze, in Lean. This is the first time in history, that I know of, when a theorem was formalized in a theorem prover, in order to resolve doubts of the mathematician who proved it. An amazing achievement. This episode tells the story, as I have understood it on line. The result apparently sparked this recent workshop .…
I
Iowa Type Theory Commute

In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.…
Welcome to Player FM!
Player FM is scanning the web for high-quality podcasts for you to enjoy right now. It's the best podcast app and works on Android, iPhone, and the web. Signup to sync subscriptions across devices.