Stephen Brookes Gödel prize recipient will deliver the 12th Annual Public Boole Lecture on Monday 16th October 18:30 pm

13 Oct 2023

This lecture is aimed at a general audience, admission is free, and everybody is welcome to attend.

Please register here for catering purposes https://forms.office.com/e/4xuPSHHJ3C

This event is organised by Michel Schellekens & John Morrison (UCC Department of Computer Science). Sponsored by the Insight Centre for Data Analytics, UCC Boole Centre for Research in Informatics, UCC Department of Computer Science, UCC School of Mathematical Sciences.

ABSTRACT OF LECTURE:

George Boole is renowned as the inventor of what became Boolean logic, now the fundamental basis of modern digital computing. Boole showed how to use mathematics to give a rigorous account of logic, and how to use symbolic operations on binary digits to solve logical problems in a systematic manner. Today, computers perform symbolic calculations at incredible speed, solving problems in areas far beyond logic, of much greater complexity than Boole can have envisioned. It is natural, then, to ask how we can hope to understand and explain what programs do, without the desire or ability to look inside the hardware and watch the binary digits fly by. The answer is again to use mathematics, taking a leaf from Boole’s book. In this talk we discuss the main ideas behind mathematical (denotational) semantics, a framework introduced by Dana Scott and Christopher Strachey for explaining program behaviour in an abstract manner, independent of hardware details. We focus on the key principles underpinning this approach, referential transparency and compositionality, and why they are important. We finish with some comments on the challenges of coping with modern multi-processors that exploit parallel evaluation to achieve great efficiency, while making it much harder to understand program behaviour abstractly.

ABOUT THE SPEAKER.

Stephen Brookes is Professor of Computer Science at Carnegie Mellon University. He obtained his BA degree in Mathematics (1978) and his PhD degree in Computer Science (1983), both from Oxford University. His PhD thesis introduced the "failures" model of Hoare's CSP. A long-term aim of his research, culminating in his foundational work for Concurrent Separation Logic (CSL), has been to facilitate the design and analysis of correct concurrent programs. He has recently begun working on semantic models for weak memory concurrency. His work on Concurrent Separation Logic was partially funded by NSF.

In the theoretical realm, almost all research papers developing concurrent program logics in the last decade are based on CSL. CSL's simplicity and structure facilitates automation. As a result, numerous tools and techniques in the research community are based on it and it is attracting attention in companies such as Microsoft, Facebook and Amazon.

Stephen Brookes and Peter W. O'Hearn received the 2016 Gödel Prize for their invention of Concurrent Separation Logic.