BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An introduction to program verification with F* - Santiago Zanella
 -Beguelin\, Microsoft Research Cambridge
DTSTART:20160714T093000Z
DTEND:20160714T101500Z
UID:TALK66803@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:Fstar (https://fstar-lang.org) is a verification-oriented prog
 ramming language that follows in the tradition of ML. Like ML\, Fstar is a
  typed\, strict\, and effectful functional programming language. However\,
  Fstar type system is significantly richer than ML's\, allowing program sp
 ecifications\, including effects\, to be stated and checked semi-automatic
 ally.\n\nTo prove that a program meets its type and effect specification\,
  the Fstar type checker uses a weakest precondition calculus to compute ve
 rification conditions\, which it then tries to discharge using the Z3 SMT 
 solver. Crucially\, there is no distinction between the language used to w
 rite programs and specifications. Consistency is maintained by verifying t
 hat specifications are pure\, terminating computations.\n\nThis talk will 
 be organized as a tutorial. I will gradually introduce the features of the
  language with the help of interactive demos. Some familiarity with functi
 onal programming languages\, specially Fsharp or ML\, can help\, but it is
  not required.\n\nThose willing to learn about advanced features of Fstar\
 , like extraction to OCaml and C\, verification of stateful programs using
  hyper heaps\, and our ongoing work on verifying the TLS protocol\, are we
 lcome to stay after the first part of the talk.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR