May 13, 2014

Microsoft Distinguished Research Lecture Series

Location: Microsoft Research Cambridge UK

Leslie Lamport – Thinking for Programmers: Rising Above the Code

Architects draw detailed blueprints before a brick is laid or a nail is hammered. Programmers and software engineers seldom do. A blueprint for software is called a specification. The need for extremely rigorous specifications before coding complex or critical systems should be obvious – especially for concurrent and distributed systems. This talk explains why some sort of specification should be written for any software.

This lecture was held on Tuesday 13 May 2014.

Prof. The Lord Darzi – Technological Innovation in Healthcare

Technological innovation has had a profound impact on human health and life expectancy over the recent history of mankind. In his lecture, Professor Darzi will discuss the key drivers of healthcare innovation, arguing that more of the same is not enough to tackle the spiralling costs and gross inequalities faced by modern healthcare systems. Outlining some of his key research highlights to date – including advances in minimally invasive, image-guided and robotic surgery – Lord Darzi will make the case for a new approach to technological innovation, which requires learning across the spectrum of low- to high-income countries, in order to champion and spread the best in frugal and low-cost design.

This lecture was held on Tuesday 18 November 2014.

Prof. Sir Tony Hoare – Laws of Programming with Concurrency

The basic Laws of Nature sought by many branches of science, as well as the basic axioms postulated in many branches of mathematics, have historically been expressed in great generality as algebraic equations, or occasionally as inequalities. Nowadays these equations provide the theoretical foundation for the design of automated tools which are widely used to help scientists and engineers in pursuit of their goals. This is the way in which Isaac Newton still contributes to mechanics, Blaise Pascal to statistics, Clark Maxwell to electronics, and George Boole to computer logic design.

How many Computer Scientists and Software Engineers are familiar with the laws which underlie their own professional practice? They are remarkably similar to the laws of arithmetic, taught even today to schoolchildren. I will present arguments that they are both generally true of computer programs, and provide the foundation for tools that are widely used in programming practice. And the laws of concurrent programming are no more complicated than those for sequential programming.

This lecture was held on Thursday 29th January 2015.

Prof. Dr. Bernhard Schölkopf – Toward Causal Machine Learning

In machine learning, we use data to automatically find dependences in the world, with the goal of predicting future observations. Most machine learning methods build on statistics, but one can also try to go beyond this, assaying causal structures underlying statistical dependences. Can such causal knowledge help prediction in machine learning tasks? We argue that this is indeed the case, due to the fact that causal models are more robust to changes that occur in real world datasets. We touch upon the implications of causal models for machine learning tasks such as domain adaptation, transfer learning, and semi-supervised learning. We also present an application to the removal of systematic errors for the purpose of exoplanet detection.

Machine learning currently mainly focuses on relatively well-studied statistical methods. Some of the causal problems are conceptually harder, however, the causal point of view can provide additional insights that have substantial potential for data analysis.

This lecture took place on Friday 15th May 2015.

Prof. Sir Timothy Gowers – What are the Prospects for Automatic Theorem Proving?

For several decades people have tried to write computer programs that can find proofs of mathematical statements. There have been some notable successes, such as a computer-discovered proof of the Robbins conjecture, which had previously been an open problem. But in general, progress has been disappointing: many problems that are well within the reach of an averagely good undergraduate are way beyond what the best programs can manage, and for a certain class of problems we seem to have reached an impasse.

There are two main approaches to automatic theorem proving: the human-oriented approach, which tries to get a computer to mimic as closely as possible the way that a human would find a proof, and the machine-oriented approach, which aims to surpass what humans can do by exploiting the vastly superior speed and memory of computers. Currently, the machine-oriented approach is more fashionable, but I shall argue that to get beyond the impasse it will be essential to return to the human-oriented approach. I shall describe some preliminary work that I have done with Mohan Ganesalingam, and speculate about how one might go about programming a computer to solve problems that for the moment cannot be solved without human ingenuity.

This lecture was held on Thursday 1st October 2015.