Running Programs in Reverse by Program Transformation

Programs produce output from input, but there is no reason why a program cannot be transformed to a reversed form. Given an output to the original program, the reversal will compute an input that could lead to the given output. One technique for generating reversal is based on control generation in which a program is realised as a set of constraints and predicates. The PhD studentship will explore this technique, and specifically develop a type discipline that makes control generation feasible and practical for program reversal.