• Login
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    Session Types, Concurrent Separation Logic & Algebra 
    •   QMRO Home
    • Queen Mary University of London Theses
    • Theses
    • Session Types, Concurrent Separation Logic & Algebra
    •   QMRO Home
    • Queen Mary University of London Theses
    • Theses
    • Session Types, Concurrent Separation Logic & Algebra
    ‌
    ‌

    Browse

    All of QMROCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects
    ‌
    ‌

    Administrators only

    Login
    ‌
    ‌

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Session Types, Concurrent Separation Logic & Algebra

    View/Open
    Hussain_A_PhD_final.pdf (463.0Kb)
    Publisher
    Queen Mary University of London
    Metadata
    Show full item record
    Abstract
    This 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.
    Authors
    Hussain, Akbar
    URI
    http://qmro.qmul.ac.uk/xmlui/handle/123456789/8503
    Collections
    • Theses [3824]
    Copyright statements
    The 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
    Twitter iconFollow QMUL on Twitter
    Twitter iconFollow QM Research
    Online on twitter
    Facebook iconLike us on Facebook
    • Site Map
    • Privacy and cookies
    • Disclaimer
    • Accessibility
    • Contacts
    • Intranet
    • Current students

    Modern Slavery Statement

    Queen Mary University of London
    Mile End Road
    London E1 4NS
    Tel: +44 (0)20 7882 5555

    © Queen Mary University of London.