Listen to a podcast, please open Podcast Republic app. Available on Google Play Store and Apple App Store.
Episode | Date |
---|---|
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 |