Some advanced examples in DCS

Update: 2023-09-25

Description

This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.

Comments

In Channel

Measure Functions and Termination of STLC

2025-11-1421:42

Schematic Affine Recursion, Oh My!

2025-08-2218:49

The Stunner: Linear System T is Diverging!

2025-08-1921:03

Terminating Computation First?

2025-08-0111:27

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

2025-05-1207:10

Krivine's Proof of FD, Using Intersection Types

2025-05-0521:35

A Measure-Based Proof of Finite Developments

2025-04-1623:24

Introduction to the Finite Developments Theorem

2025-03-2715:54

Nominal Isabelle/HOL

2025-01-3116:18

The Locally Nameless Representation

2025-01-0319:54

POPLmark Reloaded, Part 2

2024-12-2313:59

POPLmark Reloaded, Part 1

2024-12-2315:14

Introduction to Formalizing Programming Languages Theory

2024-11-2512:20

Turing's proof of normalization for STLC

2024-05-2117:39

Introduction to normalization for STLC

2024-05-1409:39

The curious case of exponentiation in simply typed lambda calculus

2024-05-0407:29

Arithmetic operations in simply typed lambda calculus

2024-05-0409:56

Some advanced examples in DCS

#box-pro-ellipsis-176440147175414{-webkit-line-clamp:2;}Some advanced examples in DCS

Some advanced examples in DCS

Aaron Stump

Some advanced examples in DCS