BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Programming and Proving with Concurrent Resources - Ilya Sergey\, 
 University College London
DTSTART:20160617T130000Z
DTEND:20160617T140000Z
UID:TALK65996@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:In the past decade\, significant progress has been made toward
 s design and development of efficient concurrent data structures and algor
 ithms\, which take full advantage of parallel computations. Due to sophist
 icated interference scenarios and a large number of possible interactions 
 between concurrent threads\, working over the same shared data structures\
 , ensuring full functional correctness of concurrent programs is challengi
 ng and error-prone.\n\nIn my talk\, through a series of examples\, I will 
 introduce Fine-grained Concurrent Separation Logic (FCSL)---a mechanized l
 ogical framework for implementing and verifying fine-grained concurrent pr
 ograms.\n\nFCSL features a principled model of concurrent resources\, whic
 h\, in combination with a small number of program and proof-level commands
 \, is sufficient to give useful specifications and verify a large class of
  state-of-the-art concurrent algorithms and data structures. By employing 
 expressive type theory as a way to ascribe specifications to concurrent pr
 ograms\, FCSL achieves scalability: even though the proofs for libraries m
 ight be large\, they are done just once.
LOCATION:FW26
END:VEVENT
END:VCALENDAR