Skip to main content

Bringing effortless refinement of data layouts to Cogent


Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller


University of NSW


The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent . This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying. In this paper, we outline our design for a data description language and data refinement framework, called Dargent, which provides the programmer with a means to specify how Cogent represents its algebraic data types. From this specification, the compiler can then generate the C code which manipulates the C data structures directly. Once fully realised, this extension will enable more code to be automatically verified by Cogent, smoother interoperability with C, and substantially improved performance of the generated code.

BibTeX Entry

    publisher        = {Springer},
    doi              = {\_9},
    booktitle        = {8th International Symposium On Leveraging Applications of Formal Methods, Verification and
    author           = {O'Connor, Liam and Chen, Zilin and Susaria, Partha and Rizkallah, Christine and Klein, Gerwin and
                        Keller, Gabi},
    month            = nov,
    volume           = {LNCS, volume 11244},
    year             = {2018},
    date             = {2018-11-5},
    title            = {Bringing Effortless Refinement of Data Layouts to {Cogent}},
    pages            = {134-149},
    address          = {Limassol, Cyprus}


Served by Apache on Linux on seL4.