On September 22, 2025, at 11 a.m., in the Nicolae Iorga Hall, UBB Central Building, the Software Engineering Group invites you to a lecture

by Professor Chin Wein Ngan from the National University of Singapore and also Professor Honoris Causa of Babes Bolyai University:

Abstract: Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters. One inherent limitation of existing specification mechanisms is its reliance on only two stages: an initial stage to denote the precondition at the start of the method and a final stage to capture the postcondition. Such two-stage specifications force abstract properties to be imposed on unknown function parameters, leading to less precise specifications for higher-order methods. To overcome this limitation, we introduce a novel extension to Hoare logic that supports multiple stages for a call-by-value higher-order language with ML-like local references. In this talk, we introduce our staged logic with its semantics, and show how it can be used to handle higher-order imperative programs, including those that arise from the use of delimited continuations (from algebraic effects).