## Up-to Techniques using Sized TypesUp-to Techniques using Sized Types ## AbstractUp-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 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 DanielssonLast updated Sat Nov 11 12:42:52 UTC 2017. |