BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Specification and Verification for Unrestricted Algebraic Effects 
 and Handling
DTSTART:20240910T110000
DTEND:20240910T120000
DTSTAMP:20260501T175925Z
UID:bc1af396ff9da99d8fbc438b6c4dd9412ffaa2c5730452cb4fca7759
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Dr Yahui Song\, Research Fellow from National University of
  Singapore (NUS)\n\nAbstract\n\nProgramming with user-defined effects and 
 effect handlers has many practical use cases involving imperative effects.
  Additionally\, it is natural and powerful to use multi-shot effect handle
 rs for non-deterministic or probabilistic programs that allow backtracking
  to compute a comprehensive outcome. Existing works for verifying effect h
 andlers are restricted in one of two ways: permitting multi-shot continuat
 ions under pure setting or allowing heap manipulation for only one-shot co
 ntinuations\, due to the employed protocol mechanism to model interactions
  between invoked effects and their handlers. This work proposes a novel ca
 lculus called Effectful Specification Logic (ESL) to support unrestricted 
 effect handlers\, where zero-/one-/multi-shot continuations can co-exist w
 ith imperative effects and higher-order constructs. ESL captures behaviors
  in stages\, and provides precise models to support invoked effects\, hand
 lers and continuations. To show its feasibility\, we prototype an automate
 d verification system for this novel specification logic\, prove its sound
 ness\, report on useful case studies\, and present experimental results. W
 ith this proposal\, we have provided an extended specification logic that 
 is capable of modeling arbitrary imperative higher-order programs with alg
 ebraic effects and continuation-enabled handlers.\n\nBio\n\nYahui is a Res
 earch Fellow in the Automated Program Repair group at NUS\, working with P
 rof Abhik Roychoudhury and Prof Wei-Ngan Chin. Her research focuses on pro
 gramming languages\, particularly functional programming\, specification\,
  and verification\, logics such as temporal logic and separation logic\, a
 nd their applications in bug finding and automated program repair. \n\nMo
 re information\n\n\n 
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR