Iowa Type Theory Commute
By Aaron Stump
Listen to a podcast, please open Podcast Republic app. Available on Google Play Store and Apple App Store.
Image by Aaron Stump
Category: Technology
Open in Apple Podcasts
Open RSS feed
Open Website
Rate for this podcast
Subscribers: 3
Reviews: 0
Episodes: 179
Description
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
| Episode | Date |
|---|---|
|
Measure Functions and Termination of STLC
|
Nov 14, 2025 |
|
Schematic Affine Recursion, Oh My!
|
Aug 22, 2025 |
|
The Stunner: Linear System T is Diverging!
|
Aug 19, 2025 |
|
Terminating Computation First?
|
Aug 01, 2025 |
|
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
|
May 12, 2025 |
|
Krivine's Proof of FD, Using Intersection Types
|
May 05, 2025 |
|
A Measure-Based Proof of Finite Developments
|
Apr 16, 2025 |
|
Introduction to the Finite Developments Theorem
|
Mar 27, 2025 |
|
Nominal Isabelle/HOL
|
Jan 31, 2025 |
|
The Locally Nameless Representation
|
Jan 03, 2025 |
|
POPLmark Reloaded, Part 1
|
Dec 23, 2024 |
|
POPLmark Reloaded, Part 2
|
Dec 23, 2024 |
|
Introduction to Formalizing Programming Languages Theory
|
Nov 25, 2024 |
|
Turing's proof of normalization for STLC
|
May 21, 2024 |
|
Introduction to normalization for STLC
|
May 14, 2024 |
|
Arithmetic operations in simply typed lambda calculus
|
May 04, 2024 |
|
The curious case of exponentiation in simply typed lambda calculus
|
May 04, 2024 |
|
More on basics of simple types
|
Apr 29, 2024 |
|
Begin Chapter on Simple Type Theory
|
Apr 19, 2024 |
|
Some advanced examples in DCS
|
Sep 25, 2023 |
|
DCS compared to termination checkers for type theories
|
Sep 19, 2023 |
|
Getting started with DCS
|
Sep 10, 2023 |
|
Introduction to DCS
|
Sep 04, 2023 |
|
Semantics of subtyping
|
Jul 24, 2023 |
|
More on type inference for simple subtypes
|
Jul 16, 2023 |
|
Subtyping, the golden key
|
Jul 09, 2023 |
|
Type inference with simple subtypes
|
Jun 30, 2023 |
|
Basics of subtyping
|
Jun 21, 2023 |
|
Begin chapter on subtyping
|
Jun 21, 2023 |
|
Last episode discussing Observational Equality Now for Good
|
Apr 13, 2023 |
|
More on observational type theory
|
Mar 23, 2023 |
|
Introduction to Observational Type Theory
|
Mar 06, 2023 |
|
Interjection: The Liquid Tensor Experiment
|
Mar 02, 2023 |
|
Extensional Martin-Loef Type Theory
|
Feb 04, 2023 |
|
Begin chapter on extensionality
|
Jan 25, 2023 |
|
Papers from Formal Methods for Blockchains 2021
|
Jan 01, 2023 |
|
Mi-Cho-Coq: Michelson formalized and applied, in Coq
|
Dec 02, 2022 |
|
Verification of Tezos smart contracts with K-Michelson
|
Nov 11, 2022 |
|
Start of Season 4: Formal Methods for Blockchain
|
Nov 07, 2022 |
|
Separation Logic II: recursive predicates
|
Sep 16, 2022 |
|
Separation Logic 1
|
Jul 25, 2022 |
|
Let's talk about Rust
|
Jul 10, 2022 |
|
Region-Based Memory Management
|
Jun 22, 2022 |
|
Introduction to verified memory management
|
Jun 05, 2022 |
|
More on Metamath
|
May 21, 2022 |
|
Metamath
|
Apr 23, 2022 |
|
The Seventeen Provers of the World
|
Apr 10, 2022 |
|
More on Lean
|
Mar 13, 2022 |
|
The Lean Prover
|
Feb 28, 2022 |
|
More on Isabelle, and the Complexity of ITPs
|
Feb 17, 2022 |
|
Isabelle/HOL
|
Jan 28, 2022 |
|
More on Agda
|
Jan 13, 2022 |
|
A look at Agda
|
Jan 10, 2022 |
|
More reflections on Coq
|
Dec 31, 2021 |
|
The Coq Proof Assistant
|
Dec 29, 2021 |
|
Introduction to Interactive Theorem Provers
|
Dec 17, 2021 |
|
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
|
Dec 11, 2021 |
|
The proof-theoretic ordinal of a logical theory
|
Nov 21, 2021 |
|
Introduction to Ordinal Analysis
|
Nov 17, 2021 |
|
An analogy for multiplicative disjunction
|
Nov 03, 2021 |
|
Linear conjunctions and disjunctions
|
Oct 29, 2021 |
|
A taste of linear logic
|
Oct 22, 2021 |
|
Structural rules, or the Curse of the Bound Variable
|
Oct 13, 2021 |
|
Why Cut Elimination is More Complicated than Normalization
|
Oct 05, 2021 |
|
Introduction to Cut Elimination
|
Sep 29, 2021 |
|
Normalization of detours for implication inferences
|
Sep 19, 2021 |
|
Normalization in natural deduction
|
Sep 18, 2021 |
|
A Brief Look at Sequent Calculus
|
Sep 16, 2021 |
|
Implication rules for natural deduction
|
Sep 14, 2021 |
|
Natural deduction: or, the bad news!
|
Sep 14, 2021 |
|
Natural Deduction
|
Sep 12, 2021 |
|
Rules of proof, standard proof systems
|
Sep 09, 2021 |
|
Different proof systems, distinguishing logical rules from domain axioms
|
Sep 02, 2021 |
|
Introduction to Proof Theory (Start of Season 3)
|
Aug 31, 2021 |
|
Modula-2
|
Jul 28, 2021 |
|
Decomposing recursions using algebras
|
Jul 13, 2021 |
|
Reassembling datatypes from functors using a fixed-point
|
Jul 11, 2021 |
|
Decomposing datatypes into functors
|
Jul 03, 2021 |
|
Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"
|
Jun 24, 2021 |
|
Modules for Mathematical Theories (MMT)
|
Jun 09, 2021 |
|
Some thoughts on module systems so far
|
May 19, 2021 |
|
A look at Agda's module system
|
May 12, 2021 |
|
Standard ML: the Newmar King-Aire of module systems
|
May 10, 2021 |
|
A look at Haskell's module system
|
Apr 27, 2021 |
|
Let's talk about modules!
|
Apr 20, 2021 |
|
Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation
|
Apr 12, 2021 |
|
Intersections and Unions in Practice; Failure of Type Preservation with Unions
|
Mar 22, 2021 |
|
Normal terms are typable with intersection types
|
Mar 05, 2021 |
|
Intersection Types Preserved Under Beta-Expansion
|
Feb 15, 2021 |
|
Introduction to Intersection Types
|
Feb 09, 2021 |
|
Deriving disjointness of constructor ranges in RelTT
|
Feb 02, 2021 |
|
Software Design and Intrinsic Identity
|
Jan 21, 2021 |
|
Identity Inclusion in Relational Type Theory
|
Jan 18, 2021 |
|
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
|
Jan 18, 2021 |
|
Equivalence of inductive and parametric naturals in RelTT
|
Dec 28, 2020 |
|
Examples in Relational Type Theory
|
Dec 23, 2020 |
|
The Semantics of Relational Types
|
Dec 23, 2020 |
|
Introducing Relational Type Theory
|
Dec 15, 2020 |
|
The Types of Relational Type Theory
|
Dec 15, 2020 |
|
On the paper "Types, Abstraction, and Parametric Polymorphism"
|
Nov 26, 2020 |
|
Explaining my encoding of a HOAS datatype, part 2
|
Nov 09, 2020 |
|
Parametric models and representation independence
|
Nov 09, 2020 |
|
Explaining my encoding of a HOAS datatype, part 1
|
Oct 19, 2020 |
|
Term models for higher-order signatures
|
Oct 19, 2020 |
|
Lambda applicative structures and interpretations of lambda abstractions
|
Oct 08, 2020 |
|
The Basic Lemma
|
Sep 30, 2020 |
|
Logical relations are not closed under composition
|
Aug 31, 2020 |
|
The definition of a logical relation
|
Aug 19, 2020 |
|
Introduction to Logical Relations
|
Aug 17, 2020 |
|
Lamping's abstract algorithm
|
Jul 25, 2020 |
|
Examples showing non-optimality of Haskell
|
Jul 15, 2020 |
|
Lambda graphs with duplicators and start of Lamping's abstract algorithm
|
Jul 03, 2020 |
|
Duplicating redexes as the central problem of optimal reduction
|
Jun 21, 2020 |
|
Introduction to optimal beta reduction
|
Jun 16, 2020 |
|
Lexicographic termination
|
Jun 03, 2020 |
|
Well-founded recursion
|
May 19, 2020 |
|
Mendler-style iteration
|
May 19, 2020 |
|
Compositional termination checking with sized types
|
Mar 30, 2020 |
|
Noncompositionality of syntactic structural-recursion checks
|
Mar 20, 2020 |
|
Structural termination
|
Mar 17, 2020 |
|
Proving Confluence for Untyped Lambda Calculus II
|
Mar 13, 2020 |
|
Proving Confluence for Untyped Lambda Calculus I
|
Mar 13, 2020 |
|
Confluence, and its use for conversion checking
|
Mar 11, 2020 |
|
Normalization and logical consistency
|
Mar 09, 2020 |
|
Normalization in type theory: where it is needed, and where not
|
Mar 06, 2020 |
|
Introduction to normalization
|
Mar 06, 2020 |
|
Proving type safety; upcoming metatheoretic properties
|
Mar 04, 2020 |
|
The progress property and the problem of axioms in type theory
|
Mar 04, 2020 |
|
Introduction to type safety
|
Mar 02, 2020 |
|
Introduction to metatheory
|
Feb 28, 2020 |
|
Definition of the Mendler encoding
|
Feb 26, 2020 |
|
The Mendler encoding and the problem of explicit recursion
|
Feb 25, 2020 |
|
The Scott encoding
|
Feb 24, 2020 |
|
More on the Parigot encoding
|
Feb 22, 2020 |
|
Introduction to the Parigot encoding
|
Feb 18, 2020 |
|
Church-encoding natural numbers
|
Feb 17, 2020 |
|
Church encoding of lists
|
Feb 15, 2020 |
|
Church encoding of the booleans
|
Feb 15, 2020 |
|
Introduction to Church encoding
|
Feb 12, 2020 |
|
Functional encodings turning the world inside out
|
Feb 11, 2020 |
|
More benefits of lambda encodings
|
Feb 07, 2020 |
|
Introduction to lambda encodings
|
Feb 07, 2020 |
|
Adding a top type and allowing non-normalizing terms
|
Feb 05, 2020 |
|
Intersection types using Curry-style typing
|
Feb 04, 2020 |
|
Curry-style versus Church-style, and the nature of type annotations
|
Jan 30, 2020 |
|
More on Computation First, and Basic Idea of Realizability
|
Jan 29, 2020 |
|
Types should be erased for executing and reasoning about programs
|
Jan 29, 2020 |
|
Why go beyond GADTs?
|
Jan 24, 2020 |
|
GADTs for programming with representations of types
|
Jan 22, 2020 |
|
Using GADTs for typed subsetting of your language
|
Jan 20, 2020 |
|
Example of programming with indexed types: binary search trees
|
Jan 16, 2020 |
|
Programming with indexed types using singletons
|
Jan 16, 2020 |
|
Limitations of indexed types that are not truly dependent
|
Jan 14, 2020 |
|
Programming with Indexed Types
|
Jan 13, 2020 |
|
Program Termination and the Curry-Howard Isomorphism
|
Jan 10, 2020 |
|
Why Curry-Howard for classical proofs is a bad idea for programming
|
Jan 07, 2020 |
|
Curry-Howard for classical logic
|
Jan 06, 2020 |
|
Dependent types and design by contract
|
Jan 04, 2020 |
|
Indexed types and Curry-Howard for first-order quantifiers
|
Jan 03, 2020 |
|
The Curry-Howard Isomorphism for Propositional Logic
|
Jan 02, 2020 |
|
The Curry-Howard Isomorphism for Induction
|
Dec 31, 2019 |
|
Constructive proofs as programs
|
Dec 22, 2019 |
|
Functors and catamorphisms
|
Dec 20, 2019 |
|
Introduction to the Curry-Howard Isomorphism
|
Dec 20, 2019 |
|
Structured Recursion Schemes for Point-Free Recursion
|
Dec 19, 2019 |
|
More on point-free programming and category theory
|
Dec 17, 2019 |
|
Point-free programming and category theory
|
Dec 17, 2019 |
|
Concise code through point-free programming
|
Dec 13, 2019 |
|
More on FP and concise code
|
Dec 12, 2019 |
|
Functional Programming and Concise Code: Type Inference
|
Dec 12, 2019 |
|
Introduction to Functional Programming
|
Dec 11, 2019 |
|
Software Engineering Considerations for Formal Methods
|
Dec 02, 2019 |
|
Power of Computer-Checked Proofs for Software
|
Dec 01, 2019 |
|
Technical reasons for lack of adoption of computer-checked proofs
|
Nov 28, 2019 |
|
Why Computer-Checked Proofs are Not Used More in Mathematics
|
Nov 27, 2019 |
|
Computer-Checked Proofs in American Research
|
Nov 26, 2019 |
|
Computer-checked proofs about software
|
Nov 24, 2019 |
|
More on Computer-Checked Proofs
|
Nov 22, 2019 |
|
Computer-checked proofs
|
Nov 21, 2019 |