Podcasts

Some advanced examples in DCS

Published: Sept. 25, 2023, 3 a.m.
Duration: 23 minutes 16 seconds

Listed in: Technology

DCS compared to termination checkers for type theories

Published: Sept. 19, 2023, 3 a.m.
Duration: 19 minutes 45 seconds

Listed in: Technology

Getting started with DCS

Published: Sept. 10, 2023, 4 a.m.
Duration: 17 minutes 23 seconds

Listed in: Technology

Introduction to DCS

Published: Sept. 4, 2023, 4 a.m.
Duration: 11 minutes 36 seconds

Listed in: Technology

Semantics of subtyping

Published: July 24, 2023, 3 a.m.
Duration: 15 minutes 20 seconds

Listed in: Technology

More on type inference for simple subtypes

Published: July 16, 2023, 2 a.m.
Duration: 9 minutes 6 seconds

Listed in: Technology

Subtyping, the golden key

Published: July 9, 2023, 3 a.m.
Duration: 9 minutes 13 seconds

Listed in: Technology

Type inference with simple subtypes

Published: June 30, 2023, 4 a.m.
Duration: 13 minutes 27 seconds

Listed in: Technology

Basics of subtyping

Published: June 21, 2023, 9 p.m.
Duration: 8 minutes 5 seconds

Listed in: Technology

Begin chapter on subtyping

Published: June 21, 2023, 3 a.m.
Duration: 16 minutes 15 seconds

Listed in: Technology

Last episode discussing Observational Equality Now for Good

Published: April 13, 2023, 5 a.m.
Duration: 12 minutes 15 seconds

Listed in: Technology

More on observational type theory

Published: March 23, 2023, 5 a.m.
Duration: 13 minutes 43 seconds

Listed in: Technology

Introduction to Observational Type Theory

Published: March 6, 2023, 5 a.m.
Duration: 10 minutes 10 seconds

Listed in: Technology

Interjection: The Liquid Tensor Experiment

Published: March 2, 2023, 6 a.m.
Duration: 12 minutes 24 seconds

Listed in: Technology

Extensional Martin-Loef Type Theory

Published: Feb. 4, 2023, 5 a.m.
Duration: 11 minutes 23 seconds

Listed in: Technology

Begin chapter on extensionality

Published: Jan. 25, 2023, 5 a.m.
Duration: 10 minutes 27 seconds

Listed in: Technology

Papers from Formal Methods for Blockchains 2021

Published: Jan. 1, 2023, 8 p.m.
Duration: 17 minutes 1 second

Listed in: Technology

Mi-Cho-Coq: Michelson formalized and applied, in Coq

Published: Dec. 2, 2022, 6 a.m.
Duration: 15 minutes 34 seconds

Listed in: Technology

Verification of Tezos smart contracts with K-Michelson

Published: Nov. 11, 2022, 5 a.m.
Duration: 14 minutes 24 seconds

Listed in: Technology

Start of Season 4: Formal Methods for Blockchain

Published: Nov. 7, 2022, 6 a.m.
Duration: 10 minutes 58 seconds

Listed in: Technology

Separation Logic II: recursive predicates

Published: Sept. 16, 2022, 4 a.m.
Duration: 11 minutes 52 seconds

Listed in: Technology

Separation Logic 1

Published: July 25, 2022, 3 a.m.
Duration: 13 minutes 26 seconds

Listed in: Technology

Let's talk about Rust

Published: July 10, 2022, 3 a.m.
Duration: 13 minutes 47 seconds

Listed in: Technology

Region-Based Memory Management

Published: June 22, 2022, 3 a.m.
Duration: 16 minutes 57 seconds

Listed in: Technology

Introduction to verified memory management

Published: June 5, 2022, 4 a.m.
Duration: 17 minutes 8 seconds

Listed in: Technology

More on Metamath

Published: May 21, 2022, 3 a.m.
Duration: 17 minutes 19 seconds

Listed in: Technology

Metamath

Published: April 23, 2022, 9 p.m.
Duration: 14 minutes 32 seconds

Listed in: Technology

The Seventeen Provers of the World

Published: April 10, 2022, 4 a.m.
Duration: 10 minutes 36 seconds

Listed in: Technology

More on Lean

Published: March 13, 2022, 4 a.m.
Duration: 15 minutes 17 seconds

Listed in: Technology

The Lean Prover

Published: Feb. 28, 2022, 4 a.m.
Duration: 14 minutes 52 seconds

Listed in: Technology

More on Isabelle, and the Complexity of ITPs

Published: Feb. 17, 2022, 4 a.m.
Duration: 16 minutes 14 seconds

Listed in: Technology

Isabelle/HOL

Published: Jan. 28, 2022, 5 a.m.
Duration: 16 minutes 54 seconds

Listed in: Technology

More on Agda

Published: Jan. 13, 2022, 1 a.m.
Duration: 13 minutes 3 seconds

Listed in: Technology

A look at Agda

Published: Jan. 10, 2022, 5 a.m.
Duration: 15 minutes 24 seconds

Listed in: Technology

More reflections on Coq

Published: Dec. 31, 2021, 11 p.m.
Duration: 18 minutes 28 seconds

Listed in: Technology

The Coq Proof Assistant

Published: Dec. 29, 2021, 4 a.m.
Duration: 15 minutes 3 seconds

Listed in: Technology

Introduction to Interactive Theorem Provers

Published: Dec. 17, 2021, 4 a.m.
Duration: 11 minutes 58 seconds

Listed in: Technology

The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0

Published: Dec. 11, 2021, 4 a.m.
Duration: 14 minutes 10 seconds

Listed in: Technology

The proof-theoretic ordinal of a logical theory

Published: Nov. 21, 2021, 5 a.m.
Duration: 12 minutes 14 seconds

Listed in: Technology

Introduction to Ordinal Analysis

Published: Nov. 17, 2021, 3 a.m.
Duration: 14 minutes 37 seconds

Listed in: Technology

An analogy for multiplicative disjunction

Published: Nov. 3, 2021, 5 a.m.
Duration: 11 minutes 24 seconds

Listed in: Technology

Linear conjunctions and disjunctions

Published: Oct. 29, 2021, 3 a.m.
Duration: 12 minutes

Listed in: Technology

A taste of linear logic

Published: Oct. 22, 2021, 4 a.m.
Duration: 11 minutes 45 seconds

Listed in: Technology

Structural rules, or the Curse of the Bound Variable

Published: Oct. 13, 2021, 4 a.m.
Duration: 12 minutes 55 seconds

Listed in: Technology

Why Cut Elimination is More Complicated than Normalization

Published: Oct. 5, 2021, 5 a.m.
Duration: 12 minutes 6 seconds

Listed in: Technology

Introduction to Cut Elimination

Published: Sept. 29, 2021, 5 a.m.
Duration: 9 minutes 3 seconds

Listed in: Technology

Normalization of detours for implication inferences

Published: Sept. 19, 2021, 9 p.m.
Duration: 12 minutes 48 seconds

Listed in: Technology

Normalization in natural deduction

Published: Sept. 18, 2021, 5 a.m.
Duration: 10 minutes 45 seconds

Listed in: Technology

A Brief Look at Sequent Calculus

Published: Sept. 16, 2021, 4 a.m.
Duration: 11 minutes 58 seconds

Listed in: Technology

Natural deduction: or, the bad news!

Published: Sept. 14, 2021, 5 a.m.
Duration: 12 minutes 24 seconds

Listed in: Technology

Implication rules for natural deduction

Published: Sept. 14, 2021, 5 a.m.
Duration: 11 minutes 37 seconds

Listed in: Technology

Natural Deduction

Published: Sept. 12, 2021, 4 a.m.
Duration: 12 minutes 10 seconds

Listed in: Technology

Rules of proof, standard proof systems

Published: Sept. 9, 2021, 4 a.m.
Duration: 12 minutes 45 seconds

Listed in: Technology

Different proof systems, distinguishing logical rules from domain axioms

Published: Sept. 2, 2021, 3 a.m.
Duration: 12 minutes 2 seconds

Listed in: Technology

Introduction to Proof Theory (Start of Season 3)

Published: Aug. 31, 2021, 5 a.m.
Duration: 18 minutes 17 seconds

Listed in: Technology

Modula-2

Published: July 28, 2021, 4 a.m.
Duration: 11 minutes 29 seconds

Listed in: Technology

Decomposing recursions using algebras

Published: July 13, 2021, 3 a.m.
Duration: 11 minutes 54 seconds

Listed in: Technology

Reassembling datatypes from functors using a fixed-point

Published: July 11, 2021, 3 a.m.
Duration: 10 minutes 16 seconds

Listed in: Technology

Decomposing datatypes into functors

Published: July 3, 2021, 5 p.m.
Duration: 13 minutes 38 seconds

Listed in: Technology

Modular datatypes: introducing Swierstra's paper "Datatypes a la Carte"

Published: June 24, 2021, 10 p.m.
Duration: 8 minutes 50 seconds

Listed in: Technology

Modules for Mathematical Theories (MMT)

Published: June 9, 2021, 3 a.m.
Duration: 11 minutes 51 seconds

Listed in: Technology

Some thoughts on module systems so far

Published: May 19, 2021, 4 a.m.
Duration: 11 minutes 40 seconds

Listed in: Technology

A look at Agda's module system

Published: May 12, 2021, 10 a.m.
Duration: 14 minutes 4 seconds

Listed in: Technology

Standard ML: the Newmar King-Aire of module systems

Published: May 10, 2021, 5 a.m.
Duration: 13 minutes 51 seconds

Listed in: Technology

A look at Haskell's module system

Published: April 27, 2021, 1 a.m.
Duration: 22 minutes 17 seconds

Listed in: Technology

Let's talk about modules!

Published: April 20, 2021, 5 a.m.
Duration: 20 minutes 38 seconds

Listed in: Technology

Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation

Published: April 12, 2021, 5 a.m.
Duration: 13 minutes 5 seconds

Listed in: Technology

Intersections and Unions in Practice; Failure of Type Preservation with Unions

Published: March 22, 2021, 5 a.m.
Duration: 13 minutes 38 seconds

Listed in: Technology

Normal terms are typable with intersection types

Published: March 5, 2021, 6 a.m.
Duration: 10 minutes 2 seconds

Listed in: Technology

Intersection Types Preserved Under Beta-Expansion

Published: Feb. 15, 2021, 6 a.m.
Duration: 12 minutes 14 seconds

Listed in: Technology

Introduction to Intersection Types

Published: Feb. 9, 2021, 5 a.m.
Duration: 11 minutes 43 seconds

Listed in: Technology

Deriving disjointness of constructor ranges in RelTT

Published: Feb. 2, 2021, 6 a.m.
Duration: 11 minutes 45 seconds

Listed in: Technology

Software Design and Intrinsic Identity

Published: Jan. 21, 2021, 4 a.m.
Duration: 9 minutes 22 seconds

Listed in: Technology

Identity Inclusion in Relational Type Theory

Published: Jan. 18, 2021, 6 p.m.
Duration: 13 minutes 47 seconds

Listed in: Technology

On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler

Published: Jan. 18, 2021, 6 a.m.
Duration: 10 minutes 52 seconds

Listed in: Technology

Equivalence of inductive and parametric naturals in RelTT

Published: Dec. 28, 2020, 6 a.m.
Duration: 14 minutes 23 seconds

Listed in: Technology

Examples in Relational Type Theory

Published: Dec. 23, 2020, 10 p.m.
Duration: 22 minutes 39 seconds

Listed in: Technology

The Semantics of Relational Types

Published: Dec. 23, 2020, 5 a.m.
Duration: 21 minutes 18 seconds

Listed in: Technology

The Types of Relational Type Theory

Published: Dec. 15, 2020, 5 a.m.
Duration: 14 minutes 50 seconds

Listed in: Technology

Introducing Relational Type Theory

Published: Dec. 15, 2020, 5 a.m.
Duration: 13 minutes 22 seconds

Listed in: Technology

On the paper "Types, Abstraction, and Parametric Polymorphism"

Published: Nov. 26, 2020, 5 a.m.
Duration: 21 minutes 19 seconds

Listed in: Technology

Parametric models and representation independence

Published: Nov. 9, 2020, 6 a.m.
Duration: 18 minutes 33 seconds

Listed in: Technology

Explaining my encoding of a HOAS datatype, part 2

Published: Nov. 9, 2020, 6 a.m.
Duration: 18 minutes 30 seconds

Listed in: Technology

Explaining my encoding of a HOAS datatype, part 1

Published: Oct. 19, 2020, 10 p.m.
Duration: 10 minutes 2 seconds

Listed in: Technology

Term models for higher-order signatures

Published: Oct. 19, 2020, 5 a.m.
Duration: 14 minutes 29 seconds

Listed in: Technology

Lambda applicative structures and interpretations of lambda abstractions

Published: Oct. 8, 2020, 4 a.m.
Duration: 10 minutes 13 seconds

Listed in: Technology

The Basic Lemma

Published: Sept. 30, 2020, 9 p.m.
Duration: 14 minutes 33 seconds

Listed in: Technology

Logical relations are not closed under composition

Published: Aug. 31, 2020, 9 p.m.
Duration: 10 minutes 12 seconds

Listed in: Technology

The definition of a logical relation

Published: Aug. 19, 2020, 4 a.m.
Duration: 10 minutes 39 seconds

Listed in: Technology

Introduction to Logical Relations

Published: Aug. 17, 2020, 4 a.m.
Duration: 12 minutes 29 seconds

Listed in: Technology

Lamping's abstract algorithm

Published: July 25, 2020, 8 p.m.
Duration: 10 minutes 15 seconds

Listed in: Technology

Examples showing non-optimality of Haskell

Published: July 15, 2020, 4 a.m.
Duration: 19 minutes 45 seconds

Listed in: Technology

Lambda graphs with duplicators and start of Lamping's abstract algorithm

Published: July 3, 2020, 8 p.m.
Duration: 22 minutes 22 seconds

Listed in: Technology

Duplicating redexes as the central problem of optimal reduction

Published: June 21, 2020, 3 a.m.
Duration: 16 minutes 6 seconds

Listed in: Technology

Introduction to optimal beta reduction

Published: June 16, 2020, 5 a.m.
Duration: 16 minutes 46 seconds

Listed in: Technology

Lexicographic termination

Published: June 3, 2020, 4 a.m.
Duration: 11 minutes 17 seconds

Listed in: Technology

Mendler-style iteration

Published: May 19, 2020, 4 a.m.
Duration: 10 minutes 35 seconds

Listed in: Technology

Well-founded recursion

Published: May 19, 2020, 4 a.m.
Duration: 15 minutes 20 seconds

Listed in: Technology

Compositional termination checking with sized types

Published: March 30, 2020, 7 p.m.
Duration: 18 minutes 37 seconds

Listed in: Technology

Noncompositionality of syntactic structural-recursion checks

Published: March 20, 2020, 4 a.m.
Duration: 13 minutes 3 seconds

Listed in: Technology

Structural termination

Published: March 17, 2020, 5 a.m.
Duration: 16 minutes 29 seconds

Listed in: Technology

Proving Confluence for Untyped Lambda Calculus II

Published: March 13, 2020, 10 p.m.
Duration: 12 minutes 12 seconds

Listed in: Technology

Proving Confluence for Untyped Lambda Calculus I

Published: March 13, 2020, 7 p.m.
Duration: 11 minutes 48 seconds

Listed in: Technology

Confluence, and its use for conversion checking

Published: March 11, 2020, 8 p.m.
Duration: 15 minutes 5 seconds

Listed in: Technology

Normalization and logical consistency

Published: March 9, 2020, 7 p.m.
Duration: 14 minutes 43 seconds

Listed in: Technology

Normalization in type theory: where it is needed, and where not

Published: March 6, 2020, 9 p.m.
Duration: 16 minutes 28 seconds

Listed in: Technology

Introduction to normalization

Published: March 6, 2020, 4 a.m.
Duration: 12 minutes 47 seconds

Listed in: Technology

Proving type safety; upcoming metatheoretic properties

Published: March 4, 2020, 9 p.m.
Duration: 13 minutes 7 seconds

Listed in: Technology

The progress property and the problem of axioms in type theory

Published: March 4, 2020, 5 a.m.
Duration: 10 minutes 13 seconds

Listed in: Technology

Introduction to type safety

Published: March 2, 2020, 11 p.m.
Duration: 14 minutes 17 seconds

Listed in: Technology

Introduction to metatheory

Published: Feb. 28, 2020, 10 p.m.
Duration: 11 minutes 54 seconds

Listed in: Technology

Definition of the Mendler encoding

Published: Feb. 26, 2020, 9 p.m.
Duration: 15 minutes 52 seconds

Listed in: Technology

The Mendler encoding and the problem of explicit recursion

Published: Feb. 25, 2020, 9 p.m.
Duration: 10 minutes 59 seconds

Listed in: Technology

The Scott encoding

Published: Feb. 24, 2020, 8 p.m.
Duration: 16 minutes 2 seconds

Listed in: Technology

More on the Parigot encoding

Published: Feb. 22, 2020, 4 a.m.
Duration: 11 minutes 32 seconds

Listed in: Technology

Introduction to the Parigot encoding

Published: Feb. 18, 2020, 11 p.m.
Duration: 11 minutes 35 seconds

Listed in: Technology

Church-encoding natural numbers

Published: Feb. 17, 2020, 11 p.m.
Duration: 11 minutes 55 seconds

Listed in: Technology

Church encoding of lists

Published: Feb. 15, 2020, 4 a.m.
Duration: 10 minutes 56 seconds

Listed in: Technology

Church encoding of the booleans

Published: Feb. 15, 2020, 3 a.m.
Duration: 11 minutes 21 seconds

Listed in: Technology

Introduction to Church encoding

Published: Feb. 12, 2020, 1 a.m.
Duration: 10 minutes 13 seconds

Listed in: Technology

Functional encodings turning the world inside out

Published: Feb. 11, 2020, 11 p.m.
Duration: 8 minutes 36 seconds

Listed in: Technology

More benefits of lambda encodings

Published: Feb. 7, 2020, 11 p.m.
Duration: 11 minutes 40 seconds

Listed in: Technology

Introduction to lambda encodings

Published: Feb. 7, 2020, 9 p.m.
Duration: 13 minutes 52 seconds

Listed in: Technology

Adding a top type and allowing non-normalizing terms

Published: Feb. 5, 2020, 1 a.m.
Duration: 14 minutes 17 seconds

Listed in: Technology

Intersection types using Curry-style typing

Published: Feb. 4, 2020, 11 p.m.
Duration: 10 minutes 39 seconds

Listed in: Technology

Curry-style versus Church-style, and the nature of type annotations

Published: Jan. 30, 2020, 11 p.m.
Duration: 13 minutes 6 seconds

Listed in: Technology

More on Computation First, and Basic Idea of Realizability

Published: Jan. 29, 2020, 10 p.m.
Duration: 15 minutes 54 seconds

Listed in: Technology

Types should be erased for executing and reasoning about programs

Published: Jan. 29, 2020, 8 p.m.
Duration: 12 minutes 40 seconds

Listed in: Technology

Why go beyond GADTs?

Published: Jan. 24, 2020, 8 p.m.
Duration: 12 minutes 25 seconds

Listed in: Technology

GADTs for programming with representations of types

Published: Jan. 22, 2020, 8 p.m.
Duration: 15 minutes 57 seconds

Listed in: Technology

Using GADTs for typed subsetting of your language

Published: Jan. 20, 2020, 7 p.m.
Duration: 14 minutes 35 seconds

Listed in: Technology

Example of programming with indexed types: binary search trees

Published: Jan. 16, 2020, 11 p.m.
Duration: 10 minutes 54 seconds

Listed in: Technology

Programming with indexed types using singletons

Published: Jan. 16, 2020, 10 p.m.
Duration: 11 minutes 49 seconds

Listed in: Technology

Limitations of indexed types that are not truly dependent

Published: Jan. 14, 2020, noon
Duration: 14 minutes 18 seconds

Listed in: Technology

Programming with Indexed Types

Published: Jan. 13, 2020, 11 p.m.
Duration: 12 minutes 2 seconds

Listed in: Technology

Program Termination and the Curry-Howard Isomorphism

Published: Jan. 10, 2020, 8 p.m.
Duration: 10 minutes 57 seconds

Listed in: Technology

Why Curry-Howard for classical proofs is a bad idea for programming

Published: Jan. 7, 2020, 1 a.m.
Duration: 14 minutes 9 seconds

Listed in: Technology

Curry-Howard for classical logic

Published: Jan. 6, 2020, 9 p.m.
Duration: 11 minutes 58 seconds

Listed in: Technology

Dependent types and design by contract

Published: Jan. 4, 2020, 2 a.m.
Duration: 9 minutes 57 seconds

Listed in: Technology

Indexed types and Curry-Howard for first-order quantifiers

Published: Jan. 3, 2020, 8 p.m.
Duration: 9 minutes 14 seconds

Listed in: Technology

The Curry-Howard Isomorphism for Propositional Logic

Published: Jan. 2, 2020, 9 p.m.
Duration: 13 minutes 25 seconds

Listed in: Technology

The Curry-Howard Isomorphism for Induction

Published: Dec. 31, 2019, 11 p.m.
Duration: 11 minutes 45 seconds

Listed in: Technology

Constructive proofs as programs

Published: Dec. 22, 2019, 5 a.m.
Duration: 9 minutes 47 seconds

Listed in: Technology

Introduction to the Curry-Howard Isomorphism

Published: Dec. 20, 2019, 8 p.m.
Duration: 15 minutes 44 seconds

Listed in: Technology

Functors and catamorphisms

Published: Dec. 20, 2019, 8 p.m.
Duration: 12 minutes 54 seconds

Listed in: Technology

Structured Recursion Schemes for Point-Free Recursion

Published: Dec. 19, 2019, 5 a.m.
Duration: 12 minutes 30 seconds

Listed in: Technology

More on point-free programming and category theory

Published: Dec. 17, 2019, 6 p.m.
Duration: 13 minutes 11 seconds

Listed in: Technology

Point-free programming and category theory

Published: Dec. 17, 2019, 6 a.m.
Duration: 6 minutes 32 seconds

Listed in: Technology

Concise code through point-free programming

Published: Dec. 13, 2019, noon
Duration: 6 minutes 31 seconds

Listed in: Technology

More on FP and concise code

Published: Dec. 12, 2019, 11 p.m.
Duration: 9 minutes 56 seconds

Listed in: Technology

Functional Programming and Concise Code: Type Inference

Published: Dec. 12, 2019, 8 p.m.
Duration: 9 minutes 7 seconds

Listed in: Technology

Introduction to Functional Programming

Published: Dec. 11, 2019, 8 p.m.
Duration: 7 minutes 52 seconds

Listed in: Technology

Software Engineering Considerations for Formal Methods

Published: Dec. 2, 2019, 4 a.m.
Duration: 16 minutes 13 seconds

Listed in: Technology

Power of Computer-Checked Proofs for Software

Published: Dec. 1, 2019, midnight
Duration: 11 minutes 47 seconds

Listed in: Technology

Technical reasons for lack of adoption of computer-checked proofs

Published: Nov. 28, 2019, 6 p.m.
Duration: 10 minutes 10 seconds

Listed in: Technology

Why Computer-Checked Proofs are Not Used More in Mathematics

Published: Nov. 27, 2019, 8 p.m.
Duration: 9 minutes 48 seconds

Listed in: Technology

Computer-Checked Proofs in American Research

Published: Nov. 26, 2019, 9 p.m.
Duration: 13 minutes 33 seconds

Listed in: Technology

Computer-checked proofs about software

Published: Nov. 24, 2019, 5 a.m.
Duration: 8 minutes 2 seconds

Listed in: Technology

More on Computer-Checked Proofs

Published: Nov. 22, 2019, 7 p.m.
Duration: 13 minutes 41 seconds

Listed in: Technology

Computer-checked proofs

Published: Nov. 21, 2019, 8 p.m.
Duration: 14 minutes 6 seconds

Listed in: Technology