Feature Modularity in Mechanized Reasoning

Benjamin Delaware

abstract

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:

  1. 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.
  2. Demonstrating how modularization of semantic properties alongside definitions enables efficient reasoning about an entire family of programs built from a common set of features.
  3. Investigating how that these techniques can aid in the semantically correct composition of interpreters for different languages.