BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Idris --- Systems Programming Meets Full Dependent Types - Edwin B
 rady (St. Andrews)
DTSTART:20110120T130000Z
DTEND:20110120T140000Z
UID:TALK29086@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:Dependent types have emerged in recent years as a promising ap
 proach\nto ensuring program correctness. However\, existing dependently ty
 ped\nlanguages such as Agda and Coq work at a very high level of\nabstract
 ion\, making it difficult to map verified programs to suitably\nefficient 
 executable code. This is particularly problematic for\nprograms which work
  with bit level data\, e.g. network packet\nprocessing\, binary file forma
 ts or operating system services. Such\nprograms\, being fundamental to the
  operation of computers in general\,\nmay stand to benefit significantly f
 rom program verification\ntechniques.  In this talk\, I will describe the 
 use of a dependently typed\nprogramming language\, Idris\, for specifying 
 and verifying\nproperties of low-level systems programs\, taking network\n
 packet processing as an extended example. I will give an overview of the\n
 distinctive features of Idris which allow it to interact with\nexternal sy
 stems code\, with precise types. I will also show how to\nintegrate tactic
  scripts and plugin decision procedures to\nreduce the burden of proof on 
 application developers. The ideas\nare readily adaptable to languages with
  related type systems.\n\nThere is a paper available from\nhttp://www.cs.s
 t-andrews.ac.uk/~eb/writings/plpv11.pdf 
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR