Menu
My Activity Hub
Podcasts
Videos
Pricing
Feedback
Tutoring
Sign Up
Log In
My Activity Hub
Podcasts
Videos
How it works
Pricing
Tutoring
Sign Up
Log In
Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Double-negation translations and CPS conversion, part 2
13 mins; April 02, 2026
Double-negation translations and CPS conversion, part 1
13 mins; March 31, 2026
What are commuting conversions in proof theory?
22 mins; March 03, 2026
What is Control Flow Analysis for Lambda Calculus?
19 mins; January 16, 2026
Measure Functions and Termination of STLC
21 mins; November 14, 2025
Schematic Affine Recursion, Oh My!
18 mins; August 22, 2025
The Stunner: Linear System T is Diverging!
21 mins; August 19, 2025
Terminating Computation First?
11 mins; August 01, 2025
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
7 mins; May 12, 2025
Krivine's Proof of FD, Using Intersection Types
21 mins; May 05, 2025
A Measure-Based Proof of Finite Developments
23 mins; April 16, 2025
Introduction to the Finite Developments Theorem
15 mins; March 27, 2025
Nominal Isabelle/HOL
16 mins; January 31, 2025
The Locally Nameless Representation
19 mins; January 02, 2025
POPLmark Reloaded, Part 1
15 mins; December 22, 2024
POPLmark Reloaded, Part 2
13 mins; December 22, 2024
Introduction to Formalizing Programming Languages Theory
12 mins; November 25, 2024
Turing's proof of normalization for STLC
17 mins; May 20, 2024
Introduction to normalization for STLC
9 mins; May 13, 2024
Arithmetic operations in simply typed lambda calculus
9 mins; May 04, 2024
The curious case of exponentiation in simply typed lambda calculus
7 mins; May 04, 2024
More on basics of simple types
15 mins; April 29, 2024
Begin Chapter on Simple Type Theory
15 mins; April 19, 2024
Some advanced examples in DCS
23 mins; September 24, 2023
DCS compared to termination checkers for type theories
19 mins; September 18, 2023
Getting started with DCS
17 mins; September 09, 2023
Introduction to DCS
11 mins; September 03, 2023
Semantics of subtyping
15 mins; July 23, 2023
More on type inference for simple subtypes
9 mins; July 15, 2023
Subtyping, the golden key
9 mins; July 08, 2023
Type inference with simple subtypes
13 mins; June 29, 2023
Basics of subtyping
8 mins; June 21, 2023
Begin chapter on subtyping
16 mins; June 20, 2023
Last episode discussing Observational Equality Now for Good
12 mins; April 13, 2023
More on observational type theory
13 mins; March 23, 2023
Introduction to Observational Type Theory
10 mins; March 05, 2023
Interjection: The Liquid Tensor Experiment
12 mins; March 02, 2023
Extensional Martin-Loef Type Theory
11 mins; February 03, 2023
Begin chapter on extensionality
10 mins; January 24, 2023
Papers from Formal Methods for Blockchains 2021
17 mins; January 01, 2023
Mi-Cho-Coq: Michelson formalized and applied, in Coq
15 mins; December 02, 2022
Verification of Tezos smart contracts with K-Michelson
14 mins; November 10, 2022
Start of Season 4: Formal Methods for Blockchain
10 mins; November 07, 2022
Separation Logic II: recursive predicates
11 mins; September 15, 2022
Separation Logic 1
13 mins; July 24, 2022
Let's talk about Rust
13 mins; July 09, 2022
Region-Based Memory Management
16 mins; June 21, 2022
Introduction to verified memory management
17 mins; June 04, 2022
More on Metamath
17 mins; May 20, 2022
Metamath
14 mins; April 23, 2022
The Seventeen Provers of the World
10 mins; April 09, 2022
More on Lean
15 mins; March 12, 2022
The Lean Prover
14 mins; February 27, 2022
More on Isabelle, and the Complexity of ITPs
16 mins; February 16, 2022
Isabelle/HOL
16 mins; January 27, 2022
More on Agda
13 mins; January 12, 2022
A look at Agda
15 mins; January 09, 2022
More reflections on Coq
18 mins; December 31, 2021
The Coq Proof Assistant
15 mins; December 28, 2021
Introduction to Interactive Theorem Provers
11 mins; December 16, 2021
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
14 mins; December 10, 2021
The proof-theoretic ordinal of a logical theory
12 mins; November 20, 2021
Introduction to Ordinal Analysis
14 mins; November 16, 2021
An analogy for multiplicative disjunction
11 mins; November 03, 2021
Linear conjunctions and disjunctions
12 mins; October 28, 2021
A taste of linear logic
11 mins; October 21, 2021
Structural rules, or the Curse of the Bound Variable
12 mins; October 12, 2021
Why Cut Elimination is More Complicated than Normalization
12 mins; October 05, 2021
Introduction to Cut Elimination
9 mins; September 29, 2021
Normalization of detours for implication inferences
12 mins; September 19, 2021
Normalization in natural deduction
10 mins; September 18, 2021
A Brief Look at Sequent Calculus
11 mins; September 15, 2021
Implication rules for natural deduction
11 mins; September 14, 2021
Natural deduction: or, the bad news!
12 mins; September 14, 2021
Natural Deduction
12 mins; September 11, 2021
Rules of proof, standard proof systems
12 mins; September 08, 2021
Different proof systems, distinguishing logical rules from domain axioms
12 mins; September 01, 2021
Introduction to Proof Theory (Start of Season 3)
18 mins; August 31, 2021
Modula-2
11 mins; July 27, 2021
Decomposing recursions using algebras
11 mins; July 12, 2021
Reassembling datatypes from functors using a fixed-point
10 mins; July 10, 2021
Decomposing datatypes into functors
13 mins; July 03, 2021
Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"
8 mins; June 24, 2021
Modules for Mathematical Theories (MMT)
11 mins; June 08, 2021
Some thoughts on module systems so far
11 mins; May 18, 2021
A look at Agda's module system
14 mins; May 12, 2021
Standard ML: the Newmar King-Aire of module systems
13 mins; May 10, 2021
A look at Haskell's module system
22 mins; April 26, 2021
Let's talk about modules!
20 mins; April 20, 2021
Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation
13 mins; April 12, 2021
Intersections and Unions in Practice; Failure of Type Preservation with Unions
13 mins; March 22, 2021
Normal terms are typable with intersection types
10 mins; March 05, 2021
Intersection Types Preserved Under Beta-Expansion
12 mins; February 15, 2021
Introduction to Intersection Types
11 mins; February 08, 2021
Deriving disjointness of constructor ranges in RelTT
11 mins; February 02, 2021
Software Design and Intrinsic Identity
9 mins; January 20, 2021
Identity Inclusion in Relational Type Theory
13 mins; January 18, 2021
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
10 mins; January 18, 2021
Equivalence of inductive and parametric naturals in RelTT
14 mins; December 28, 2020
Examples in Relational Type Theory
22 mins; December 23, 2020
Click here to see more
‹ Prev
1
2
Next ›
