The University of New South Wales

Connecting choreography languages with verified stacks


Alejandro Gomez-Londono and Johannes Åman Pohjola


Chalmers University of Technology

UNSW Sydney


With ever increasing availability of verified stacks capable of guaranteeing end-to-end correctness on applications—like compilers (CakeML, CompCert) or even critical software systems (seL4)—one can now realistically write a program, along with a proof describing any desirable property, and have it compiled into a correct executable implementation of the original program. However, most of these approaches can only really deal with sequential programs and provide no support for reasoning about the correctness of multiple (con-current) programs. To address these shortcomings, we propose a choreographic language where the behavior of a system consisting of several endpoints, is described on a global level, that can be subsequently projected and compiled into its individual components. We are developing an end-to-end proof of correctness that ensures i) the deadlock-freedom of the generated set of endpoints and ii) the preservation of all behavior of the system down to the binary level. Our implementation uses the verified CakeML compiler as a backend and takes advantages of its verified stack.

BibTeX Entry

    isbn             = {9788273684509},
    publisher        = {N/A},
    note             = { at Nordic Workshop on Programming Theory},
    month            = oct,
    paperurl         = {},
    year             = {2018},
    booktitle        = {Nordic Workshop on Programming Theory},
    title            = {Connecting Choreography Languages With Verified Stacks},
    author           = {Gomez-Londono, Alejandro and {\AA}man Pohjola, Johannes},
    address          = {Oslo, Norway},
    date             = {2018-10-24}