Title: A Domain-Specific Language for the Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks

Author: Assaf Kfoury, Boston University

Date: May 11, 2011

Abstract: Flow networks are inductively defined, assembled from small 
networks or modules to produce arbitrarily large ones, with 
interchangeable functionally-equivalent parts. We carry out this 
induction formally using a domain-specific language (DSL). Associated 
with our DSL is a typing system (or static semantics), a system of 
formal annotations that enforce desirable properties of flow networks as 
invariants across their interfaces. A prerequisite for a type theory is 
a formal semantics, i.e., a rigorous definition of the entities that 
qualify as feasible flows through the networks, possibly restricted to 
satisfy additional efficiency or safety requirements. We carry out this 
in two ways, as a denotational semantics and as an operational (or 
reduction) semantics.