One common and effective approach to reuse is to decompose a system
into modules representing \textit{features}. New variants can then
be built by combing these features in different ways. This thesis
proposes that proofs establishing semantic properties of a system
can be similarly decomposed and reused to prove properties for novel
feature combinations. Features can cut across the standard
modularity boundaries, presenting a fundamental challenge to modular
reasoning. The proposed contributions are threefold:
-
Showing how the mechanized syntax, semantics and meta-theory
proofs of a programming language can be effectively modularized
into features that can be composed in different ways to build
programming languages with fully mechanized meta-theory.
-
Demonstrating how modularization of semantic
properties alongside definitions enables efficient reasoning about
an entire family of programs built from a common set of features.
-
Investigating how that these techniques can aid in the
semantically correct composition of interpreters for different
languages.