Research Fellows Directory
Dr James Cheney
University of Edinburgh
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.