PhD Proposal: Ben Delaware Date: Tuesday, Feb 12 Time: 3:00 PM Place: GDC 7.808 Title of dissertation: Feature Modularity in Mechanized Reasoning Abstract: One common and effective approach to reuse is to decompose a system into modules representing 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.