A type system for extracting functional specifications from memory-safe imperative programs. - Paul He; Eddy Westbrook; Brent Carmer; Chris Phifer; Valentin Robert; Karl Smeltzer; Andrei Stefanescu; Aaron Tomb; Adam Wick; Matthew Yacavone; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

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)

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)