Title: Safe Compositional Specification of Network Systems With Polymorphic, Constrained Types

Authors: Likai Liu and Assaf Kfoury, Computer Science Department, 
Boston University

Date: October 25, 2006

Abstract:

In the framework of iBench research project, our previous work created
a domain specific language TRAFFIC [BUCS-TR-2005-015] that facilitates
specification, programming, and maintenance of distributed
applications over a network. It allows safety property to be
formalized in terms of types and subtyping relations. Extending upon
our previous work, we add Hindley-Milner style polymorphism
[Milner:JCSS-1978-v17] with constraints [Odersky:TPOS-1999-v5] to the
type system of TRAFFIC. This allows a programmer to use for-all
quantifier to describe types of network components, escalating power
and expressiveness of types to a new level that was not possible
before with propositional subtyping relations. Furthermore, we design
our type system with a pluggable constraint system, so it can adapt to
different application needs while maintaining soundness.

In this paper, we show the soundness of the type system, which is not 
syntax-directed but is easier to do typing derivation. We show that 
there is an equivalent syntax-directed type system, which is what a 
type checker program would implement to verify the safety of a network 
flow. This is followed by discussion on several constraint systems: 
polymorphism with subtyping constraints, Linear Programming, and 
Constraint Handling Rules (CHR) [Fruhwirth:JLP-1998-v37]. Finally, we 
provide some examples to illustrate workings of these constraint 
systems.