Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 14:30 - 14:55 at Noh Theater - Session 2 Chair(s): Kathleen Fisher

We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.

Mon 19 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

13:40 - 14:55
Session 2Research Papers at Noh Theater
Chair(s): Kathleen Fisher Tufts University
13:40
25m
Talk
A New Verified Compiler Backend for CakeML
Research Papers
Yong Kiam Tan IHPC at A*STAR, Singapore, Magnus O. Myreen Chalmers University of Technology, Sweden, Ramana Kumar Data61 at CSIRO, Australia, Anthony Fox University of Cambridge, UK, Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia
DOI
14:05
25m
Talk
Sequent Calculus as a Compiler Intermediate Language
Research Papers
Paul Downen University of Oregon, USA, Luke Maurer University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft Research, UK
DOI
14:30
25m
Talk
Refinement through Restraint: Bringing Down the Cost of Verification
Research Papers
Liam O'Connor UNSW, Australia, Zilin Chen UNSW, Australia, Christine Rizkallah University of Pennsylvania, USA, Sidney Amani UNSW, Australia, Japheth Lim Data61, Australia, Toby Murray University of Melbourne, Australia, Yutaka Nagashima Data61, Australia, Thomas Sewell UNSW, Australia, Gerwin Klein UNSW, Australia
DOI