BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:dd2ab5e8aaef9322bbd919683370e167
DTSTAMP:20260406T093618Z
SUMMARY:Higher-order functions in the verification-aware programming langua
 ge Dafny (K. Rustan M. Leino)
DESCRIPTION:Abstract:\nWe add higher-order functions to Dafny\, a programmi
 ng language designed for reasoning and verification.  Our design of the h
 igher-order functions separates their types from their specifications\, mu
 ch like the types of a method’s parameters are separated from the pre/po
 st-condition specification of the method.  The verifier translates the us
 e of higher-order functions into first-order verification conditions to be
  discharged by Boogie/Z3.  I will demo the Dafny system using higher-orde
 r functions in the presence of heap side effects Joint work with Dan Rosé
 n.\nBio:\nK. Rustan M. Leino is a Principal Researcher in the Research in 
 Software Engineering (RiSE) group at Microsoft Research and Visiting Profe
 ssor in the Department of Computing at Imperial College London.  His rese
 arch interests include a focus on programming tools\, both mental and mech
 anical.
URL:https://www.imperial.ac.uk/events/104961/higher-order-functions-in-the-
 verification-aware-programming-language-dafny-k-rustan-m-leino/
DTSTART;TZID=Europe/London:20150120T140000
DTEND;TZID=Europe/London:20150120T150000
LOCATION:United Kingdom
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:STANDARD
DTSTART:20150120T140000
TZNAME:GMT
TZOFFSETTO:+0000
TZOFFSETFROM:+0000
END:STANDARD
END:VTIMEZONE
END:VCALENDAR