BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On the Use of Typing for Static Logical Verification: RCF and Refi
 nement Types - Noah Ohrner\, St Catharine's College
DTSTART:20191204T190000Z
DTEND:20191204T193000Z
UID:TALK135808@talks.cam.ac.uk
CONTACT:Matthew Ireland
DESCRIPTION:Proving program correctness is becoming an increasingly popula
 r area of research as computers are used in applications where security or
  correctness is of utmost human or economic importance. However\, many cur
 rent standards require either runtime overhead or providing reference impl
 ementations of algorithms in specific languages to feed into logic engines
 . This talk will explore the applications of refinement types to design a 
 strong type system which can enforce program safety according to a logical
  specification. The type system will be developed in parallel with a a fun
 ctional language similar to ML which can model concurrency\, mutable state
  and other imperative programming features\, improving on runtime or refer
 ence implementation schemes. Lastly\, it will mention two languages implem
 enting a similar verification type system and their potential uses in veri
 fying security-critical software we interact with on a daily basis.
LOCATION:Wolfson Hall\, Churchill College
END:VEVENT
END:VCALENDAR