Up-to Techniques using Sized Types

Up-to Techniques using Sized Types
Nils Anders Danielsson
In POPL 2018. Future DOI: 10.1145/3158131. [pdf, highlighted Agda code, zip file with code]

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.

Nils Anders Danielsson
Last updated Sat Nov 11 12:42:52 UTC 2017.