Feature modularity in mechanized reasoning
| dc.contributor.advisor | Cook, William Randall | |
| dc.creator | Delaware, Benjamin James | en |
| dc.date.accessioned | 2014-01-15T19:42:28Z | en |
| dc.date.issued | 2013-12 | en |
| dc.date.submitted | December 2013 | en |
| dc.date.updated | 2014-01-15T19:42:29Z | en |
| dc.description | text | en |
| dc.description.abstract | Complex systems are naturally understood as combinations of their distinguishing characteristics or \definit{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. | en |
| dc.description.department | Computer Science | |
| dc.format.mimetype | application/pdf | en |
| dc.identifier.uri | http://hdl.handle.net/2152/22867 | en |
| dc.language.iso | en_US | en |
| dc.subject | Programming language metatheory | en |
| dc.subject | Modular reasoning | en |
| dc.title | Feature modularity in mechanized reasoning | en |
| thesis.degree.department | Computer Sciences | en |
| thesis.degree.discipline | Computer Science | en |
| thesis.degree.grantor | The University of Texas at Austin | en |
| thesis.degree.level | Doctoral | en |
| thesis.degree.name | Doctor of Philosophy | en |