MSc Defence by Xiaomo Yao
Reversible Computation with Types
Reversible computing is an emerging research area that studies about the backward as well as the forward determinism of models of computation. A traditional computing device, such
The approach taken in this thesis arises from a functional programmer’s perspective: The invertibility and compositionality of partial functions are surveyed as crucial properties in a functional programming language for reversible computation. A type system, BT, inspired by computation in symmetric monoidal categories, is formally defined. By embedding the information-preserving injection types by
Based upon the specified type system, we propose a general-purpose functional programming language, BEYOND, that is reversibility-aware, in the sense that both conventional and reversible computations are supported, and types also provide a static guarantee for the reversibility of programs aside from their correctness. The invertibility of pattern matching on algebraic data types, as well as on refined primitive types, can be inferred algorithmically.
Furthermore, heuristics based on induction are developed so as to infer the invertibility of recursive functions with fixed-point semantics.
Supervisors: Robin Kaarsgaard and Robert Glück.