Modular and Extensible Programming Language Metatheory
Static program analyses are an important tool for
ensuring the absence of run-time errors. A faulty
analysis is ofentimes worse than none at all,
providing users with a false sense of
security. This makes it particularly important
that static analyses are sound, only validating
programs that are actually error-free. Designers
typically establish soundness via a mathematical
meta-theory proof connecting the analysis to a
formal description of a language's semantics. To
ensure the correctness of these intricate proofs,
researchers commonly mechanize them in
computerized proof assistants. These mechanized
proofs can be both tedious and labor-intensive,
but this effort results in a foundational proof of
the correctness of the analysis, which is
automatically conferred onto any analyzed
program.
These mechanized proof developments are
artifacts that, much like source code, can be
adapted and extended with new features, enabling
the development of variant
languages. Unfortunately, the standard approach to
language extension is essentially to copy the
existing formalization, modify that copy, and then
patch up the proofs. The effects of an extension
can be woven throughout the meta-theory proofs of
a language, making it difficult to both identify
and apply the meta-theory changes required by a
new feature. This project attempts to solve these
challenges by developing sounds and modular
approaches to extend programming languages with
new features, allowing programming language
researchers to better leverage existing mechanized
formalizations of languages, enabling innovation
without compromising soundness.
Representative Papers: