Show simple item record

dc.contributor.authorHussain, Akbar
dc.identifier.citationHussain, A.2013. Session Types, Concurrent Separation Logic & Algebra.Queen Mary University of London.en_US
dc.description.abstractThis dissertion explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Concurrent Separation Logic are formalisms that support independent reasoning about concurrent processes, and our motivating question is whether their modularity springs from the same source despite the distance between their models. We first translate a small language we call Baby Session Types (BST), into a ‘basic’ version of Concurrent Separation Logic (BCSL), and we show that the translation is sound. We then describe a model for Separation Logic (SL) based on Actions, which exhibits some of the structure of a Concurrent Kleene Algebra, an algebra where operators for parallel and sequential composition are linked by a version of the exchange law from category theory. The model connects the algebraic notions to locality concepts that underlie Separation Logic. We then move on to provide a more general construction of an algebra model of BCSL, which can be built from (Baby) Session Types. Thus, we end up with a model that brings together concepts from all of Session Types, Separation Logic, and Concurrent Kleene Algebra. Thus, the model links diverse models of concurrency. In addition to this it suggests alterations of the algebraic axioms as well as the foundational models underlying Separation Logic. It is hoped that, apart from these specific results, this dissertation can in some modest way contribute to unification in concurrency theory, a theory (or theories) based presently on diverse models.en_US
dc.description.sponsorshipEngineering and Physical Sciences Research Council; School of Electronic Engineering and Computer Science, Queen Mary, University of Londonen_US
dc.publisherQueen Mary University of Londonen_US
dc.subjectElectronic Engineeringen_US
dc.titleSession Types, Concurrent Separation Logic & Algebraen_US
dc.rights.holderThe copyright of this thesis rests with the author and no quotation from it or information derived from it may be published without the prior written consent of the author

Files in this item


This item appears in the following Collection(s)

  • Theses [3919]
    Theses Awarded by Queen Mary University of London

Show simple item record