Interaction Trees

Source Code

Documentation

• Development version (master branch)
• Version 5.0.0

List of publications about or closely related to Interaction Trees.

2019

• From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
  by Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
  CPP 2019 coq vst testing plclub

2020

• Interaction Trees: Representing Recursive and Impure Programs in Coq
  by Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
  POPL 2020 coq monads coinduction plclub
• An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
  by Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
  CPP 2020 coq coinduction plclub
• Connecting Higher-Order Separation Logic to a First-Order Outside World
  by William Mansky, Wolf Honoré, Andrew W. Appel
  ESOP 2020 coq vst

2021

• Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
  by Lucas Silver, Steve Zdancewic
  POPL 2021 coq monads coinduction plclub
• Model-based Testing of Networked Applications
  by Yishuai Li, Benjamin C. Pierce, Steve Zdancewic
  ISSTA 2021 coq testing plclub
• Verifying an HTTP Key-Value Server with Interaction Trees and VST
  by Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic
  ITP 2021 coq vst testing plclub
• A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
  by Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
  OOPSLA 2021 coq plclub
• Modular, Compositional, and Executable Formal Semantics for LLVM IR
  by Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
  ICFP 2021 coq monads plclub
• Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
  by Simon Foster, Chung-Kil Hur, Jim Woodlock
  CONCUR 2021 isabelle concurrency

2022

• C4: Verified Transactional Objects
  by Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
  OOPSLA 2022 coq concurrency plclub
• Program Adverbs and Tlön Embeddings
  by Yao Li, Stephanie Weirich
  ICFP 2022 coq plclub
• Formal Reasoning About Layered Monadic Interpreters
  by Irene Yoon, Yannick Zakowski, Steve Zdancewic
  ICFP 2022 coq monads plclub
• Formally Verified Animation for RoboChart using Interaction Trees
  by Kangfeng Ye, Simon Foster, Jim Woodcock
  ICFEM 2022 isabelle concurrency
• Conditional Contextual Refinement
  by Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur
  Draft coq concurrency
• Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
  by Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
  Draft coq concurrency plclub