Thu 11 Jan 2018 15:50 - 16:15 at Watercourt - Dependent Types Chair(s): Karl Crary

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.

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

15:50 - 16:40
Dependent TypesResearch Papers at Watercourt
Chair(s): Karl Crary Carnegie Mellon University
Up-to Techniques Using Sized Types
Research Papers
Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
Decidability of Conversion for Type Theory in Type Theory
Research Papers
Andreas Abel Gothenburg University, Joakim Öhman IMDEA Software Institute, Andrea Vezzosi Chalmers University of Technology