Skip to main content

From Denotational Semantics to Facebook Engineering

Professor Peter O'Hearn ( Engineering Manager at Facebook and Professor of Computer Science, University College, London )

Denotational Semantics is an approach to describing the meanings of programming languages, originating in the work of Scott and Strachey at Oxford in the 1960s and 1970s. Facebook is a software company whose products in 2015 are used by over a billion people. I began my career working in an abstract branch, based on category-theoretic models, of the already abstract subject of denotational semantics, and now I find myself working on much more concrete problems within the fast-paced engineering org at Facebook.

In this talk, I will describe how these seemingly distant areas are linked. I chart a line of development from models of programs and logics to automatic program verification/analysis techniques that are in deployment at Facebook.

The journey will take in a number of concepts from the computer science logician's toolkit --  including categorical logic and model theory, denotational semantics, the Curry-Howard isomorphism, Substructural Logic, Hoare Logic and Separation Logic, abstract interpretation, compositional program analysis, the frame problem, and abductive inference.

 

Share this: