Iowa Type Theory Commute

By: Aaron Stump
Listen for free

  • Summary

  • Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
    © 2025 Iowa Type Theory Commute
    Show more Show less
Mathematics Science
Show more Show less
Episodes
  • A Measure-Based Proof of Finite Developments

    A Measure-Based Proof of Finite Developments
    Apr 16 2025

    I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.
    Show more Show less
    23 mins
  • Introduction to the Finite Developments Theorem

    Introduction to the Finite Developments Theorem
    Mar 27 2025

    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.
    Show more Show less
    16 mins
  • Nominal Isabelle/HOL

    Nominal Isabelle/HOL
    Jan 31 2025

    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.

    Show more Show less
    16 mins
adbl_web_global_use_to_activate_webcro768_stickypopup

What listeners say about Iowa Type Theory Commute

Average customer ratings

Reviews - Please select the tabs below to change the source of reviews.

Audible.com reviews

Amazon reviews
No Reviews are Available