Dijkstra monads forever: termination-sensitive specifications for interaction trees. - Lucas Silver; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Semantics for Noninterference with Interaction Trees. - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (ECOOP, 2023)

Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification. - Lucas Silver; Eddy Westbrook; Matthew Yacavone; Ryan Scott (ECOOP, 2023)

Semantics for Noninterference with Interaction Trees (Artifact). - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (Dagstuhl Artifacts Ser., 2023)

Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact). - Lucas Silver; Eddy Westbrook; Matthew Yacavone; Ryan Scott (Dagstuhl Artifacts Ser., 2023)