Iowa Type Theory Commute
Iowa Type Theory Commute
Aaron Stump
Some advanced examples in DCS
23 minutes Posted Sep 25, 2023 at 3:00 am.
0:00
23:16
Download MP3
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.