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)