Programming Languages Seminar: Shaan Nagy

Abstract: The semantics of Hoare-style logics typically restrict the sorts of properties one can prove. In Hoare Logic, one can only prove overapproximations of single-state program semantics; in Incorrectness Logic, one can prove underapproximations. Proving even simple hyperproperties (properties that require reasoning about multiple executions at once) like monotonicity requires more complex logics. To unify these contexts, Hyper Hoare Logic (HHL) lifts program semantics and logical asserti