BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Local Temporal Reasoning - Eric Koskinen\, New York University
DTSTART:20140627T093000Z
DTEND:20140627T103000Z
UID:TALK53210@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:I will discuss our recent development of the first method for 
 proving temporal logic properties of programs written in higher-order lang
 uages such as C#\, F#\, Haskell\, Ocaml\, Perl\, Ruby\, Python\, etc. By d
 istinguishing between the finite traces and infinite traces in the specifi
 cation\, we obtain rules that permit us to reason about the temporal behav
 ior of program parts via a type-and-effect system\, which is then able to 
 compose these facts together to prove the overall target property of the p
 rogram.\nThe type system alone is strong enough to derive many temporal sa
 fety properties\, for example when using dependent (refinement) types and 
 temporal effects. We also show how existing techniques can be used as orac
 les to provide liveness information (e.g. termination) about program parts
  and that the type-and-effect system can combine this information with tem
 poral safety information to derive nontrivial temporal properties.\nOur wo
 rk has application toward verification of higher-order software\, as well 
 as modular strategies for interprocedural programs.\n\nJoint work with Tac
 hio Terauchi. To appear in LICS 2014.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR