BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Logical Reasoning for Higher-Order Functions with Local State - No
 buko Yoshida  (Imperial College)
DTSTART:20071026T130000Z
DTEND:20071026T140000Z
UID:TALK7297@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:This talk presents an extension of Hoare logic for\nhigher-ord
 er functions with ML-like local reference generation.  Local\nreferences m
 ay be generated dynamically and exported outside their\nscope\, may store 
 higher-order functions and may be used to construct\ncomplex mutable data 
 structures. This primitive is captured logically\nusing a predicate assert
 ing reachability of a reference name from a\npossibly higher-order datum a
 nd quantifiers over hidden\nreferences.\n\nWe explore the logic's descript
 ive and reasoning power with\nnon-trivial programming examples combining h
 igher-order procedures and\ndynamically generated local state.  Axioms for
  reachability and\nlocal invariant play a central role for reasoning about
  the examples.\n\nThe logic enjoys the three completeness properties: rela
 tive completeness\,\na logical characterisation of the contextual congruen
 ce and\nderivability of characteristic formulae.\n\nJoint work with\nKohei
  Honda and\nMartin Berger.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR