All Episodes
Iowa Type Theory Commute — 191 episodes · page 1 of 2
Autoformalization of Fermat's Last Theorem
A Fireball of Alpha
Solving Quadratic Word Equations
A little bit about word equations
Coercive subtyping and coherence
A Strange Deal, Explained
A Strange Deal
Great paper: The Calculated Typer
Double-negation translations and CPS conversion, part 2
Double-negation translations and CPS conversion, part 1
What are commuting conversions in proof theory?
What is Control Flow Analysis for Lambda Calculus?
Measure Functions and Termination of STLC
Schematic Affine Recursion, Oh My!
The Stunner: Linear System T is Diverging!
Terminating Computation First?
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
Krivine's Proof of FD, Using Intersection Types
A Measure-Based Proof of Finite Developments
Introduction to the Finite Developments Theorem
Nominal Isabelle/HOL
The Locally Nameless Representation
POPLmark Reloaded, Part 2
POPLmark Reloaded, Part 1
Introduction to Formalizing Programming Languages Theory
Turing's proof of normalization for STLC
Introduction to normalization for STLC
The curious case of exponentiation in simply typed lambda calculus
Arithmetic operations in simply typed lambda calculus
More on basics of simple types
Begin Chapter on Simple Type Theory
Some advanced examples in DCS
DCS compared to termination checkers for type theories
Getting started with DCS
Introduction to DCS
Semantics of subtyping
More on type inference for simple subtypes
Subtyping, the golden key
Type inference with simple subtypes
Basics of subtyping
Begin chapter on subtyping
Last episode discussing Observational Equality Now for Good
More on observational type theory
Introduction to Observational Type Theory
Interjection: The Liquid Tensor Experiment
Extensional Martin-Loef Type Theory
Begin chapter on extensionality
Papers from Formal Methods for Blockchains 2021
Mi-Cho-Coq: Michelson formalized and applied, in Coq
Verification of Tezos smart contracts with K-Michelson
Start of Season 4: Formal Methods for Blockchain
Separation Logic II: recursive predicates
Separation Logic 1
Let's talk about Rust
Region-Based Memory Management
Introduction to verified memory management
More on Metamath
Metamath
The Seventeen Provers of the World
More on Lean
The Lean Prover
More on Isabelle, and the Complexity of ITPs
Isabelle/HOL
More on Agda
A look at Agda
More reflections on Coq
The Coq Proof Assistant
Introduction to Interactive Theorem Provers
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
The proof-theoretic ordinal of a logical theory
Introduction to Ordinal Analysis
An analogy for multiplicative disjunction
Linear conjunctions and disjunctions
A taste of linear logic
Structural rules, or the Curse of the Bound Variable
Why Cut Elimination is More Complicated than Normalization
Introduction to Cut Elimination
Normalization of detours for implication inferences
Normalization in natural deduction
A Brief Look at Sequent Calculus
Natural deduction: or, the bad news!
Implication rules for natural deduction
Natural Deduction
Rules of proof, standard proof systems
Different proof systems, distinguishing logical rules from domain axioms
Introduction to Proof Theory (Start of Season 3)
Modula-2
Decomposing recursions using algebras
Reassembling datatypes from functors using a fixed-point
Decomposing datatypes into functors
Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"
Modules for Mathematical Theories (MMT)
Some thoughts on module systems so far
A look at Agda's module system
Standard ML: the Newmar King-Aire of module systems
A look at Haskell's module system
Let's talk about modules!
Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation
Intersections and Unions in Practice; Failure of Type Preservation with Unions
Normal terms are typable with intersection types