All episodes
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