CS Colloquium on Sept. 24 at 3PM

Title: A Type-Disciplined Approach to Developing Resources
       and Applications for the World-Wide Web
       (Doctoral Dissertation Defense)

Speaker: Adam D. Bradley, Boston University
         http://cs-people.bu.edu/artdodge

Abstract:

Programming of stand-alone computer systems has long benefited from formal
methods for system specification, programming, and execution; such
formalisms lend themselves to precise mechanical verification of a system's
desired properties.  Type systems particularly have proven effective at
reining in the unbounded expressive power of programming languages without
excessively burdening the programmer.  It is the position of this thesis
that such techniques can be adapted to suit the programming of open
networked systems.  Thereby, benefits can be realized to the correctness
and stability of the individual components of said systems, to the
precision with which such systems are specified, and to the correctness,
reliability, predictability, and interoperability of networked programs and
systems as a whole.

In support of this concept, five formal methods (the P, B, and X type
systems, the L type model, and the CHAIN methodology) are developed which
reflect the promotion of ``flows'' to first-class programming language
citizens accessible to type systems and other formal correctness tools.  We
employ ``flow'' as a generic abstraction for mechanisms which affect the
transaction of state among components of a networked system to achieve its
desired end.  These five systems largely reflect novel applications of
existing technologies and systems to various forms of flows; two also
employ a novel type construct, the ``stacked type syntax'', which captures
nesting relationships within data representations.

The P type system enforces constraints upon the flow of system state
changes by restricting program side-effects to predictable classes.  The B
type systems identify flows of information from server back-end sources
(basis data) to representations thus identifying potential representational
inconsistencies within the system.  The X type systems enforce XML
well-formedness upon the output streams (flows) of programs.  The L type
model imposes structure upon the specification of the HTTP protocol's
content modeland supports a more precise declaration of the semantics of
its syntax (i.e., its interpretive flow).  The CHAIN methodology offers a
systematic approach to assessing correctness of systems which construct
communication channels (flows) by composing arbitrarily long sequences of
intermediaries, and are thus not amenable to direct global verification.

Thesis Committee:
-----------------
Major Advisor: Azer bestavros, Computer Science Dept., B.U.
Second Reader: Assaf J. Kfoury, Computer Science Dept., B.U.
Third Reader: Richard West, Computer Science Dept., B.U.
Fourth Reader: Ibrahim Matta, Computer Science Dept., B.U.
Committee Chair: Wayne Snyder, Computer Science Dept., B.U.