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.