BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:KAT on a Wire: A Foundation for Network Programming - David Walker
 \, Princeton University
DTSTART:20130805T100000Z
DTEND:20130805T110000Z
UID:TALK46390@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Recent years have seen growing interest in high-level programm
 ing languages for networks. But the design of these languages has been lar
 gely ad hoc\, driven more by the needs of applications and the capabilitie
 s of network hardware than by foundational principles. The lack of a seman
 tic foundation has left language designers with little guidance in determi
 ning how to incorporate new features\, and programmers without a means to 
 reason precisely about their code. \n\nThis paper presents NetKAT\, a new 
 language for programming networks that is based on a solid mathematical fo
 undation and comes equipped with a sound and complete equational theory. W
 e describe the design of NetKAT\, including primitives for filtering\, mod
 ifying\, and transmitting packets\; operators for combining programs in pa
 rallel and in sequence\; and a Kleene star operator. We show that NetKAT i
 s an instance of a canonical and well-studied mathematical structure calle
 d a Kleene algebra with tests (KAT)\, and prove that its equational theory
  is sound and complete with respect to its denotational semantics. Finally
 \, we present practical applications of the equational theory including sy
 ntactic techniques for checking reachability properties\, proving the corr
 ectness of compilation and optimization algorithms\, and establishing a no
 n-interference property that ensures isolation between programs.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR