Up-to Techniques Using Sized Types

Up-to Techniques Using Sized Types
Nils Anders Danielsson
Draft. [pdf, accompanying 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 convenient to use in practice.

On the more theoretical side a class of up-to techniques intended to capture a natural mode of use of such 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 Wed Sep 6 14:02:38 UTC 2017.