Peter Landin (1930 - 2009) was a pioneer whose ideas underpin modern
computing. In the 1950s and 1960s, Landin showed that programs could be
defined in terms of mathematical functions, translated into functional expressions in the lambda calculus, and their meaning calculated with an abstract mathematical machine. Compiler writers and designers of modern-day programming languages alike owe much to Landin's pioneering work.
Each year, a leading figure in computer science will pay tribute to
Landin's contribution to computing through a public seminar. This year's seminar is entitled “Building trustworthy refactoring tools” and will be given by Professor Simon Thompson (University of Kent).
6.00pm Welcome & Introduction
6.05pm Peter Landin Semantics Seminar
Building trustworthy refactoring tools
Professor Simon Thompson
University of Kent
7.20pm Drinks Reception
Refactorings are program transformations that are intended to change the
way that a program works without changing what it does. Refactoring is
used to make programs more readable, easier to maintain and extend, or to improve their efficiency. These changes can be complex and wide-ranging,
and so tools have been built to automate these transformations.
Because refactoring involves changing program source code, someone who uses
a refactoring tool needs to be able to trust that the tool will not
break their code. In this talk I'll explore what is meant by "preserving meaning" in practice, and how we provide various levels of assurance for refactoring’s, ranging from testing to full, machine assisted,
verification. While the context is tools for functional programming
languages like Haskell, Erlang and OCaml, the conclusions apply more
widely, for instance to object-oriented languages.
About the speaker
Simon Thompson is Professor of Logic and Computation at the University of
Kent. Functional programming is his main research field, but he has
worked in various aspects of logic, and testing as well. He is the author
of books on Haskell, Miranda, Erlang and constructive type theory. The work reported here is a result of collaborations with colleagues past and