Complex systems are naturally understood as
combinations of their distinguishing characteristics or
features. Distinct features differentiate between variations of
configurable systems and also identify the novelties of
extensions. The implementation of a conceptual feature is often
scattered throughout an artifact, forcing designers to understand the
entire artifact in order to reason about the behavior of a single
feature. It is particularly challenging to independently develop novel
extensions to complex systems as a result.
This dissertation shows
how to modularly reason about the implementation of conceptual
features in both the formalizations of programming languages and
object-oriented software product lines. In both domains, modular
verification of features can be leveraged to reason about the behavior
of artifacts in which they are included: fully mechanized metatheory
proofs for programming languages can be synthesized from independently
developed proofs, and programs built from well-formed feature
modules are guaranteed to be well-formed without needing to be
typechecked. Modular reasoning about individual features can
furthermore be used to efficiently reason about families of languages
and programs which share a common set of features.