Iowa Type Theory Commute

Aaron Stump
Iowa Type Theory Commute

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

  1. 12 MAJ

    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 MAJ

    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 MARS

    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. 2024-12-23

    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. 2024-12-23

    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
Visa alla (175)

Betyg och recensioner

5
av 5
3 betyg

Om

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

Information

  • Skapad av
    Aaron Stump
  • Aktiva år
    2019 - 2025
  • Avsnitt
    175
  • Åldersgräns
    Barnvänligt
  • Copyright
    © 2025 Iowa Type Theory Commute
  • Programmets webbplats
    Iowa Type Theory Commute

Du kanske också gillar

Logga in för att lyssna på vuxet innehåll.

Följ programmet

Logga in eller registrera dig för att följa program, spara avsnitt och få de senaste uppdateringarna.
Välj land eller region

Afrika, Mellanöstern och Indien

Stillahavsområdet

Europa

Latinamerika och Karibien

USA och Kanada