SWIT presentation with Prof. Dr. Chin Wei Ngan from National University of Singapore

On January 15th, we hosted the SWIT presentation with Prof. Dr. Chin Wei Ngan from the National University of Singapore, who delivered an insightful talk titled “Specification and Verification for Unrestricted Algebraic Effects and Handling.”

During the session, Prof. Ngan introduced Effectful Specification Logic (ESL), a groundbreaking calculus designed to address limitations in verifying user-defined effects and handlers. ESL supports unrestricted zero-/one-/multi-shot continuations alongside imperative effects and higher-order constructs, offering precise models for behaviors, effects, handlers, and continuations.

The presentation also highlighted an automated verification system, proofs of soundness, case studies, and experimental results, demonstrating ESL's potential to model complex imperative programs with algebraic effects and continuation-enabled handlers.