Up-to Techniques Using Sized Types

Learn about up-to techniques and their implementation through sized types in this 24-minute conference presentation from POPL 2018. Explore how size-preserving functions can be used to construct proofs of bisimilarity, with Nils Anders Danielsson from the University of Gothenburg/Chalmers University of Technology demonstrating practical applications through various examples. Examine the theoretical framework of a specific class of up-to techniques that aligns with Pous's concept of 'functions below the companion'. Discover both the capabilities and limitations of this approach through examples of functions that cannot be made size-preserving. Delve into topics including coinduction, sized types, and the companion concept while learning how these techniques can simplify complex proof constructions.