Coq, the world's best macro assembler !
Speaker(s) : Pierre-Evariste DAGAND (INRIA)
With Nick Benton and Andrew Kennedy (Microsoft Research Cambridge), I have worked on CoqOS, a Coq library for programming and verifying x86 assembly programs. This library offers an operational semantics of (a significant subset of) the x86 CPU, a certified assembler, and a separation logic for reasoning about x86 assembly programs. In this framework, I have implemented a regular expression compiler and proved its correctness : the resulting x86 code accepts a word iff the regexp matches that word.
I will first give a brief introduction to CoqOS, demonstrating a few of its salient features. I shall put a special emphasis on its program logic, which is obtained by elegant algebraic means. I will then illustrate its workings with some of the programming and proving patterns used in my certified compiler.
Julia.Lawall (at) nulllip6.fr