Measure Functions and Termination of STLC

Iowa Type Theory Commute by Aaron Stump

In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some process or program, by assigning a measure to each program, and showing that as the p...View more