PLClub Discussion Group

POPL Practice Talks

Talks

1. Interaction Trees: Representing Recursive and Impure Programs in Coq

Presenter: Li-yao Xia
Time: 12:30pm - 1pm

Interaction trees (ITrees) are a general-purpose data structure in Coq for representing the behaviors of recursive programs that interact with their environments. ITrees, a coinductive variant of “free monads,’’ 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. And 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 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.

We have implemented ITrees and their associated theory as a Coq library, which mechanizes classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library make heavy use of coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq’s coinduction tactics.

To demonstrate the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given as ITree-based denotational semantics. Unlike previous results using operational techniques, this bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.

2. An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction

Presenter: Yannick Zakowski
Time: 1pm - 1:30pm

Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization.

This paper gives a novel presentation of an equational theory for reasoning about structures up to weak bisimulation. The theory is both compositional, making it suitable for defining general-purpose lemmas, and also incremental, meaning that the bisimulation can be created interactively. To prove the theory’s soundness, this paper also introduces generalized parameterized coinduction, which addresses expressivity problems of earlier works and provides a practical framework for coinductive reasoning. The paper presents the resulting equational theory for streams, but the technique applies to other structures too.

All of the results in this paper have been proved in Coq, and the generalized parameterized coinduction framework is available as a Coq library.

SRC Posters

Time: 1pm - 1:30pm

3. Combinatorial Testing for Algebraic Data Types

Presenter: Harry Goldstein

Combinatorial or “t-way” testing provides a principled way of testing the possible behaviors of a system. While this approach is well studied for systems that operate on simple input parameters, there has been relatively little exploration of its use for more complex structured data. We propose a definition of t-way testing that is generalized to algebraic data types, including recursive types. We define combinatorial coverage using regular tree expressions as descriptions of tests, and we provide a sketch of an algorithm for generating covering test sets that are guaranteed to catch certain classes of bugs. This abstract presents work in progress.

4. Through the Interaction Forest: Modeling Concurrency in Coq with Interaction Trees

Presenter: Irene Yoon

How do we specify concurrent programs? In the presence of concurrency, programs must be viewed as components that interact with their environment. This intuition has developed into bisimulation, an observational equational theory for reasoning about concurrent programs. Interaction Trees(ITrees) represent impure and recursive programs in Coq. In essence, it is a coinductive variant of a free monad. Its free monadic structure provide a modular method of reasoning about effects. Coinduction allows ITrees to represent recursive programs as infinite data structures and sets ground to a straightforward application of bisimulation. Weak bisimulation, a method of encapsulating internal interactions within a component, observes behavioral equivalence of ITrees. This equational theory serves as a clean, modular proof technique for equating impure, recursive programs. A natural extension of Interaction Trees, then, is to use its bisimilarity proof techniques for reasoning about concurrent programs in Coq. In this extended abstract, we present a preliminary model of concurrent, and possibly interleaving Interaction Trees.