Searching for Canonical Representations of Programs – REPRO

The REPRO project aims to: - deepen our understanding of the structure of computer programs by discovering canonical representations for fundamental programming languages, - explore their applications to the problems of program equivalence checking and program synthesis Two programs with code source may actually behave in the exact same way. A canonical representation is a different way to represent programs that better captures their identity: two different representations correspond to observably-different programs. We know very little about these canonical representations, except in fairly idealized settings --- the simply-typed lambda-calculus. We propose to study canonical representations for larger classes of programming languages, that is statically typed, functional programming languages. This requires new theoretical developments, but could have many applications for equivalence checking (verifying refactoring) and program synthesis (guessing a program from a partial spec)