## 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 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 DanielssonLast updated Wed Sep 6 14:02:38 UTC 2017. |