All Episodes
Iowa Type Theory Commute — 187 episodes
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
Intersection Types Preserved Under Beta-Expansion
Introduction to Intersection Types
Deriving disjointness of constructor ranges in RelTT
Software Design and Intrinsic Identity
Identity Inclusion in Relational Type Theory
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
Equivalence of inductive and parametric naturals in RelTT
Examples in Relational Type Theory
The Semantics of Relational Types
The Types of Relational Type Theory
Introducing Relational Type Theory
On the paper "Types, Abstraction, and Parametric Polymorphism"
Parametric models and representation independence
Explaining my encoding of a HOAS datatype, part 2
Explaining my encoding of a HOAS datatype, part 1
Term models for higher-order signatures
Lambda applicative structures and interpretations of lambda abstractions
The Basic Lemma
Logical relations are not closed under composition
The definition of a logical relation
Introduction to Logical Relations
Lamping's abstract algorithm
Examples showing non-optimality of Haskell
Lambda graphs with duplicators and start of Lamping's abstract algorithm
Duplicating redexes as the central problem of optimal reduction
Introduction to optimal beta reduction
Lexicographic termination
Mendler-style iteration
Well-founded recursion
Compositional termination checking with sized types
Noncompositionality of syntactic structural-recursion checks
Structural termination
Proving Confluence for Untyped Lambda Calculus II
Proving Confluence for Untyped Lambda Calculus I
Confluence, and its use for conversion checking
Normalization and logical consistency
Normalization in type theory: where it is needed, and where not
Introduction to normalization
Proving type safety; upcoming metatheoretic properties
The progress property and the problem of axioms in type theory
Introduction to type safety
Introduction to metatheory
Definition of the Mendler encoding
The Mendler encoding and the problem of explicit recursion
The Scott encoding
More on the Parigot encoding
Introduction to the Parigot encoding
Church-encoding natural numbers
Church encoding of lists
Church encoding of the booleans
Introduction to Church encoding
Functional encodings turning the world inside out
More benefits of lambda encodings
Introduction to lambda encodings
Adding a top type and allowing non-normalizing terms
Intersection types using Curry-style typing
Curry-style versus Church-style, and the nature of type annotations
More on Computation First, and Basic Idea of Realizability
Types should be erased for executing and reasoning about programs
Why go beyond GADTs?
GADTs for programming with representations of types
Using GADTs for typed subsetting of your language
Example of programming with indexed types: binary search trees
Programming with indexed types using singletons
Limitations of indexed types that are not truly dependent
Programming with Indexed Types
Program Termination and the Curry-Howard Isomorphism
Why Curry-Howard for classical proofs is a bad idea for programming
Curry-Howard for classical logic
Dependent types and design by contract
Indexed types and Curry-Howard for first-order quantifiers
The Curry-Howard Isomorphism for Propositional Logic
The Curry-Howard Isomorphism for Induction
Constructive proofs as programs
Introduction to the Curry-Howard Isomorphism
Functors and catamorphisms
Structured Recursion Schemes for Point-Free Recursion
More on point-free programming and category theory
Point-free programming and category theory
Concise code through point-free programming
More on FP and concise code
Functional Programming and Concise Code: Type Inference
Introduction to Functional Programming
Software Engineering Considerations for Formal Methods
Power of Computer-Checked Proofs for Software
Technical reasons for lack of adoption of computer-checked proofs
Why Computer-Checked Proofs are Not Used More in Mathematics
Computer-Checked Proofs in American Research
Computer-checked proofs about software
More on Computer-Checked Proofs
Computer-checked proofs