Substructural Meta-Theory of a Type-Safe Language forWeb Programming

This paper introduces an abstract web programming language, QWeSST, and a methodology for proving properties of formalisms, such are QWeSST, that are parallel, distributed and concurrent. At its core, QWeSST is a small functional programming language extended with primitives for mobile code and remote procedure calls, two distinguishing features of web programming. It supports a localized view of typechecking and of evaluation, which reflects the way we program web applications and web services. We have developed a prototype implementation for QWeSST and used it to elegantly write simple web applications that are however not easily expressed using current web technology. We give two semantics for QWeSST, one is standard and models a naive form of single-threaded evaluation, the other is maximally parallel and exploits a presentation of its typing and execution behaviors based on an extended form of substructural operational semantics. It augments standard inference rules with a construction that realizes parametric multiset comprehension, which makes it convenient to capture ensemble-level behaviors. We prove that both semantics are type safe, the former using traditional methods, the latter by developing a proof methodology that parallels the multiset-oriented presentation of the semantics.