From Denotational Semantics to Facebook Engineering

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.