Iowa Type Theory Commute

Aaron Stump
  • 5.0 (3)
  • TECHNOLOGY

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

  1. 12 MAY

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

    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.

    7 min

  2. 5 MAY

    Krivine's Proof of FD, Using Intersection Types

    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.

    22 min

  3. 16 APR

    A Measure-Based Proof of Finite Developments

    I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer.  See also the write-up at my blog.

    23 min

  4. 27 MAR

    Introduction to the Finite Developments Theorem

    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.

    16 min

  5. 31 JAN

    Nominal Isabelle/HOL

    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.

    16 min

  6. 3 JAN

    The Locally Nameless Representation

    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.

    20 min

  7. 23/12/2024

    POPLmark Reloaded, Part 2

    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.

    14 min

  8. 23/12/2024

    POPLmark Reloaded, Part 1

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

    15 min
See All (175)

Ratings & Reviews

5
out of 5
3 Ratings

About

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

Information

  • Creator
    Aaron Stump
  • Years Active
    2019 - 2025
  • Episodes
    175
  • Rating
    Clean
  • Copyright
    © 2025 Iowa Type Theory Commute
  • Show Website
    Iowa Type Theory Commute

You Might Also Like