Talks by Dana Scott, ACM A.M. Turing award 1976, Thursday 26 May, Friday 27th May and Wednesday 1 June

Dana Scott, ACM A.M. Turing award 1976, gave a very well attended talk at Imperial on Stochastic λ-Calculus on Thursday 26th of May. The talk and lecture were part of a series of talks by Dana Scott in London in May and June, listed below.

Stochastic λ-Calculus. Thursday 26 May, Imperial College London.

Abstract: It is shown how the operators in the “graph model” for λ-calculus (which can function as a programming language for Recursive Function Theory) can be expanded to allow for “random combinators”.  The result then is a semantics for a new language for random algorithms.  The author wants to make a plea for finding applications.


Lambda Calculus: Then & Now. Thursday 26 May 2016, British Computer Society, London

Abstract: A very fast development in the early 1930’s following Hilbert’s codification of Mathematical Logic led to the Incompleteness Theorems, Computable Functions, Undecidability Theorems, and the general formulation of Recursive Function Theory. The so-called Lambda Calculus played a key role. The history of these developments will be traced, and the much later place of Lambda Calculus in Mathematics and Programming-Language Theory will be outlined.

Types and Type-free Lambda Calculus Friday 27th May, University College London

Abstract:  Denotational semantics started in Oxford in late 1969. It was hoped that domain theory would provide a basis both for recursive definitions in programs and recursive definitions of semantical structures. Early troubles were encountered in using tops and bottoms, and soon researchers turned to operational semantics. Others wanted to expand work to communicating and parallel processes. Axiomatic and synthetic theories did not solve the problems, and as a result much research effort in domain theory faded. Late work by Reynolds and collaborators, however, has opened up new and promising approaches for programming-language semantics. Perhaps the much simplified modeling using enumeration operators can spark some new investigations, especially since it is so easy to add a rich type structure to the calculus.

Why Mathematical Proof? Joint Maths Colloquium/EECS Distinguished seminar by Prof. Dana ScottWednesday 1 June, Queen Mary University of London, London


Annual Conference and Report, 2015

The Three National Cyber Security Programme sponsored cyber security Research Institutes are organising their joint annual highlights conference, at the Department for Business Innovation and Skills in October 2015. The purpose of the conference is to present this leading edge initiative and its outcomes to decision-makers and leaders from academia, government and industry.

Download the Annual report 2015 (PDF)

Annual Report, 2014

The Research Institute in Automated Program Analysis and Verification Annual Report provides an overview of the developments and achievements in 2014, our first year of operation.

Download the Annual report 2014 (PDF)

FMATS3 at Microsoft Research, 2014

FMATS3 on 1-2 May 2014 was co-organised by the Research Institute.

FMATS3 was held at Microsoft Research Cambridge on 1st and 2nd May 2014. This year we had additional talks from the individual projects affiliated to the Research Institute in Automated Program Analysis and Verification (RI2).  The event was attended by 47  participants comprising researchers from academia, industry and government and included talks on 16 different topics (see On the 2nd day, we had a poster session along with bite-size introductions from nine winners of the “PhD Prizes”. In the  discussion session on the future of the FMATS workshop, it was agreed that the FMATS community should be opened to other complementary networks like CryptoForma and adopt ideas from other similar events like NSA’s HCSS conference.

The future organisation of FMATS will be led by the Director of RI2, Professor Philippa Gardner of Imperial College, London.

To keep updated on future FMATS events email Anuj Sood, Program Manager of RI2 at (replace xx by @).