Iowa Type Theory Commute

Some advanced examples in DCS

September 24, 2023 Aaron Stump Season 4 Episode 19
Some advanced examples in DCS
Iowa Type Theory Commute
More Info
Iowa Type Theory Commute
Some advanced examples in DCS
Sep 24, 2023 Season 4 Episode 19
Aaron Stump

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.

Show Notes

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.