Engineering Commons^™

Irrelevance, Polymorphism, And Erasure In Type Theory, Richard Nathan Mishra-Linger

Dissertations and Theses

Dependent type theory is a proven technology for verified functional programming in which programs and their correctness proofs may be developed using the same rules in a single formal system. In practice, large portions of programs developed in this way have no computational relevance to the ultimate result of the program and should therefore be removed prior to program execution. In previous work on identifying and removing irrelevant portions of programs, computational irrelevance is usually treated as an intrinsic property of program expressions. We find that such an approach forces programmers to maintain two copies of commonly used datatypes: a …

Directflow: A Domain-Specific Language For Information-Flow Systems, Andrew P. Black, Chuan-Kai Lin

Computer Science Faculty Publications and Presentations

Programs that process streams of information are commonly built by assembling reusable information-flow components. In some systems the components must be chosen from a pre-defined set of primitives; in others the programmer can create new custom components using a general-purpose programming language. Neither approach is ideal: restricting programmers to a set of primitive components limits the expressivity of the system, while allowing programmers to define new components in a general-purpose language makes it difficult or impossible to reason about the composite system. We advocate defining information-flow components in a domain-specific language (DSL) that enables us to infer the properties of …

Metamodeling Aspects Of Model Conceptualization, Wayne W. Wakeland

Systems Science Faculty Publications and Presentations

This paper suggests a technique for improving the conceptualization of models. The key aspect of this technique is to set aside the main model for a period of time during the model conceptualization process and focus on building a "watchdog" submodel. The primary purpose of the watchdog submodel is to assure that the main model remains internally consistent during its operation. In the experience of this author, such a submodel can help to identify model conceptualization errors and to determine if a model is sufficiently "robust" to adequately replicate the behavior of the system being modeled.

This is not a …