Regular Expressions and Multiparty Session Types with Applications to Workflow Based Verification of User Interfaces

PhD defence by Lasse Nielsen  


With the aim of producing a framework for clinical practice guideline modeling and reasoning, we consider regular expressions and multiparty session types and investigate and develop their ability to express example guidelines, verify treatment compliance, verify specification compliance and static verification of user interface implementations.

For regular expressions we have studied the extension of regular expression matching to regular expression parsing, and have developed a compact bit-coding of the resulting parse trees that can be generated directly by efficient parsing algorithms without ever materializing the uncompressed parse-trees. Our contributions also include a sound and complete axiomatization of regular expression language inclusion based on the general coinduction rule, with an operational interpretation of proofs as a translation of parse-trees from one regular expression to the other, which can work directly on the compact bit-codes as well. The new axiomatization is so powerfull that the rules in the existing axiomatizations by Salomaa, Kozen and Grabmayer are derivable, which provides these axiomatizations with an operational interpretation.

For session types, we have extended the asynchronous multiparty session types by Honda, Yoshida and Carbone with a social interaction construct, which enables a natural representation of workflows as session types while preserving the original soundness properties of the original typesystem. This enables compliance verification of workflow implementations by static type-checking. We have studied the expressiveness of the added construct, and prove that it can be encoded using the existing constructs, at the cost of an exponential blowup in the size of the terms and types. We have implemented a prototype interpretor and type checker for the full language, which enables the implemented workflows to be tested and demonstrated.

Assessment committee:

Chairman: Associate Professor Andrzej Filinski, Department of Computer Science, University of Copenhagen, Denmark
Professor Dexter Kozen, Cornell University, Department of Computer Science, USA
Professor Jakob Rehof, Technische Universität Dortmund, Fraunhofer-Institut für Software- und Systemtechnik ISST, Germany

Academic supervisors:

Professor Fritz Henglein, Department of Computer Science, University of Copenhagen, Denmark
Associate Professor Thomas Hildebrandt, IT University of Copenhagen, Denmark

For an electronic copy of the thesis, please contact Jette Giovanni Møller,