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.
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.
Everyone uses math libraries. Surprisingly, mainstream math libraries do not produce correct results for several thousands of inputs. Developers are seldom aware of them, which affects reproducibility and portability. We describe our new method for synthesizing elementary functions that produces correct results for all inputs but is also significantly faster than the state of the art libraries, which have been optimized for decades.
We give an introduction to reflective towers of interpreters, a semantic model of reflection with a user level interpreted by a meta level interpreted by a meta meta level and so on.
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.
Sensitivity properties study how the output of a program changes when we make small changes to its input. How can we reason about sensitivity of programs that have probabilistic behavior?
A brief farewell from Mike Hicks, outgoing co-editor at PL Perspectives, and a brief hello by Adrian Sampson, co-editor incoming!
How can types and formal reasoning tools improve the lives of people who write software? This is the focus of the HATRA (Human Aspects of Types and Reasoning Assistants) workshop. At the 2020 meeting, we discussed exciting opportunities for these key PL techniques to make developers more effective.
When developing massively distributed, interactive applications, programmers must select mechanisms that balance consistency, performance, and availability, which can be challenging. New research is looking at ways to automate this selection, with provable guarantees.
