Select Page

PL Perspectives

Perspectives on computing and technology from and for those with an interest in programming languages.
The Story of the Flash Fill Feature in Excel

The Story of the Flash Fill Feature in Excel

My POPL 2011 “Flash Fill” paper was the most important turning point in my research career. I went from searching for the hardest problem I can solve to searching for the simplest problem that will have the most impact. It sensitized me to customer connection and enlightened me to how practical requirements can inspire foundational research ideas and directions. And most of all, it led to a blissful connection with my loved ones.

Read more...

Specification Synthesis with Constrained Horn Clauses

Specification Synthesis with Constrained Horn Clauses

The problem of program verification is to find whether a program meets its specification. But if a program calls functions whose bodies are missing, the verification aims at finding the most general implementations of these functions. In this post we show how advances in automated reasoning allow for doing it efficiently.

Read more...

Making Software Sandboxing Practical using Language-based Techniques

Making Software Sandboxing Practical using Language-based Techniques

Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. The idea of SFI is old. Its use in production, to sandbox third-party libraries in Firefox, is new. We describe the PL techniques—notably static information flow control—that were key to deploying SFI in practice and their use in tackling software security more generally.

Read more...