Some advanced examples in DCS Iowa Type Theory Commute

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.