This paper introduces ctrees, a monad for modeling nondeterministic, recursive, and impure
programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds …

This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential
subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified …

Transactional objects combine the performance of classical concurrent objects with the high-
level programmability of transactional memory. However, verifying the correctness of …

We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol
parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for …

Simulation and formal verification are important complementary techniques necessary in
high assurance model-based systems development. In order to support coherent results, it is …

Free monads (and their variants) have become a popular general-purpose tool for
representing the semantics of effectful programs in proof assistants. These data structures …

Multiparty session types is a typing discipline used to write specifications, known as global
types, for branching and recursive message-passing systems. A necessary operation on …

Noninterference is the strong information-security property that a program does not leak
secrets through publicly-visible behavior. In the presence of effects such as nontermination …

Choice trees have recently been introduced as a general structure for defining the semantics
of programming languages with a wide variety of features and effects. In this article we focus …

Temporal logics for hyperproperties have recently emerged as an expressive specification
technique for relational properties of reactive systems. While the model checking problem for …