Iowa Type Theory Commute podcast

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

26:28

Squid Game is back—and this time, the knives are out. In the thrilling Season 3 premiere, Player 456 is spiraling and a brutal round of hide-and-seek forces players to kill or be killed. Hosts Phil Yu and Kiera Please break down Gi-hun’s descent into vengeance, Guard 011’s daring betrayal of the Game, and the shocking moment players are forced to choose between murdering their friends… or dying. Then, Carlos Juico and Gavin Ruta from the Jumpers Jump podcast join us to unpack their wild theories for the season. Plus, Phil and Kiera face off in a high-stakes round of “Hot Sweet Potato.” SPOILER ALERT! Make sure you watch Squid Game Season 3 Episode 1 before listening on. Play one last time. IG - @SquidGameNetflix X (f.k.a. Twitter) - @SquidGame Check out more from Phil Yu @angryasianman , Kiera Please @kieraplease and the Jumpers Jump podcast Listen to more from Netflix Podcasts . Squid Game: The Official Podcast is produced by Netflix and The Mash-Up Americans.…

Iowa Type Theory Commute

Поширити

Головна серій•Feed

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

175 епізодів

Iowa Type Theory Commute

17 subscribers

updated рік тому

Поширити

Головна серій•Feed

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

175 епізодів

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

Усі епізоди

1
Correction: the Correct Author of the Proof from Last Episode, and an AI flop 7:10

8 weeks тому7:10

7: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.

1
Krivine's Proof of FD, Using Intersection Types 21:35

9 weeks тому21:35

21: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.

1
A Measure-Based Proof of Finite Developments 23:24

12 weeks тому23:24

23: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.

1
Introduction to the Finite Developments Theorem 15:54

15 weeks тому15:54

15: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.…

1
Nominal Isabelle/HOL 16:18

22 weeks тому16:18

16:18

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.

1
The Locally Nameless Representation 19:54

26 weeks тому19:54

19:54

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.…

1
POPLmark Reloaded, Part 1 15:14

28 weeks тому15:14

15:14

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

1
POPLmark Reloaded, Part 2 13:59

28 weeks тому13:59

13:59

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.

1
Introduction to Formalizing Programming Languages Theory 12:20

32 weeks тому12:20

12: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.

1
Turing's proof of normalization for STLC 17:39

1 year тому17:39

17:39

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.

1
Introduction to normalization for STLC 9:39

1 year тому9:39

9:39

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).…

1
Arithmetic operations in simply typed lambda calculus 9:56

1 year тому9:56

9: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.…

1
The curious case of exponentiation in simply typed lambda calculus 7:29

1 year тому7:29

7: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.…

1
More on basics of simple types 15:45

1 year тому15:45

15:45

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

1
Begin Chapter on Simple Type Theory 15:41

1 year тому15:41