PLClub Discussion Group


From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR

Dec 13 2019
Yannick Zakowski

The DeepSpec research project is a cross institution, cross projectinvestigation to push further the science of specification and verificationof software artifacts. Its ambition is crystallized into four qualities thatspecifications should have: they should be rich, live, two-sided and formal.

In this talk, we will focus on the design and implementation of InteractionTrees (ITrees), a general-purpose data-structure for representing in Coqpotentially divergent, effectful, programs. ITrees are built out ofuninterpreted events and their continuations They support compositionalconstruction of interpreters from event handlers, which give meaning toevents by defining their semantics as monadic actions. They are expressiveenough to represent impure and potentially nonterminating, mutually recursivecomputations in Coq. Finally, they give rise to a theory enabling equationalreasoning, up to weak bisimulation, about ITrees and monadic computationsbuilt from them. In contrast to other approaches, ITrees are executable viacode extraction.

ITrees are expressive enough to serve as a language of specification for mostprojects of the DeepSpec ecosystem, making them a sort of Franca Lingua forformal specification, and helping in connecting projects together.Furthermore, their ability to be extracted make them compatible withambitions of liveness and two-sidedness.

In a second part of this talk, we will focus on how ITrees are used in one ofthe DeepSpec projects in particular: Vellvm. More specifically, we will givean account of the ongoing effort to use ITrees as a mean to define a modularformal semantics of LLVM IR.