Reference. CDSL Version 1: Simplifying Verification with Linear Types [oconnor-kamkcr-2014]

October 2014
Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen, Christine Rizkallah
NICTA Technical Report
Available from TS

We introduce a purely functional domain specific language, CDSL, which aims to substantially reduce the cost of producing efficient, verified file system code. Given an executable specification of a file system, the CDSL compiler generates C code and, when fully implemented, will also generate an Isabelle/HOL proof linking the specification and the C implementation. We present two operational semantics for CDSL: (1) a value semantics, well suited for verification, and (2) an update semantics, which can be mapped to efficient C code. We outline the equivalence proof between these two semantics and discuss how the type system guarantees properties like termination, correct error handling, absence of memory leaks and aliasing.