Room 206 (2nd floor, badged access)
19 December 2019 - 14h00
From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR
by Yannick Zakowski from University of Pennsylvania
Abstract: The DeepSpec research project is a cross institution, cross project investigation to push further the science of specification and verification of software artifacts. Its ambition is crystallized into four qualities that specifications should have: they should be rich, live, two-sided and formal.
In this talk, we will focus on the design and implementation of _Interaction Trees_ (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.
ITrees are expressive enough to serve as a language of specification for most projects of the DeepSpec ecosystem, making them a sort of Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.
In a second part of this talk, we will focus on how ITrees are used in one of the DeepSpec projects in particular: Vellvm. More specifically, we will give an account of the ongoing effort to use ITrees as a mean to define a modular formal semantics of LLVM IR.
