Up-to techniques using sized types

Abstract

Up-to techniques are used to make it easier - or feasible - to construct, for instance, proofs of bisimilarity. This text shows how many up-to techniques can be framed as size-preserving functions, using sized types to keep track of sizes. Through a number of examples it is argued that this approach to up-to techniques is often convenient to use in practice. Some examples of functions that cannot be made size-preserving are also included, in order to illustrate the limits of the approach. On the more theoretical side a class of up-to techniques intended to capture a natural mode of use of size-preserving functions is defined. This class turns out to correspond closely to "functions below the companion", a notion recently introduced by Pous.