Scheme: University Research Fellowship
Organisation: University of Edinburgh
Dates: Dec 2013-Dec 2016
Summary: Programming language research relies on proofs of correctness for formal systems involving name-binding. Name-binding means the occurrence of certain symbols as tokens for unknown objects, such as variables in qualified logical formulas or integrals in calculus. Nearly all practical programming languages employ name-binding, but reasoning about languages with name-binding is currently much more complex than reasoning about simple algebraic languages, and such proofs can easily contain hard-to-find mistakes. Computer-aided reasoning would be helpful but is not yet powerful enough to help with the analysis of real programming languages. Similarly, most provenance techniques have been developed for simple domain-specific languages, and extending such techniques to full programming languages with name-binding appears difficult.
My fellowship research has built upon an influential approach developed over the past ten years by Gabbay and Pitts. Their key insight was that alpha-equivalence (that is, equivalence up to consistent renaming of bound names) can be defined formally in terms of simpler operations such as swapping (exchanging two names) and freshness (checking whether a name appears in an expression); these operations have better equational properties than the traditional, non-invertible substitution or renaming operations. This is an exciting research area both because it is based on elegant theory and because it offers the opportunity to dramatically increase the scope of mechanised reasoning techniques for language design and verification.
Dates: Oct 2008-Dec 2013