Interaction trees: representing recursive and impure programs in Coq
Abstract
Interaction trees (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of “free monads,” 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. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 20, 2019
- Source ID
- 10.1145/3371119
Entities
People
- Benjamin C. Pierce
- Chung-kil Hur
- Gregory Malecha
- Li-yao Xia
- Paul He
- Steve Zdancewic
- Yannick Zakowski
Organizations
- National Research Foundation of Korea
- National Science Foundation
- Office of Naval Research
- Seoul National University
- University of Pennsylvania