Personal tools
You are here: Home Events Milner Lectures Milner Lecture 2019

Milner Lecture 2019

This year's lecture will be given by Professor Dexter Kozen.

What
When May 16, 2019
from 04:00 PM to 05:00 PM
Where Informatics Forum, G.07
Add event to calendar vCal
iCal

Milner Lecture 2019

Abstract

Networks have received widespread attention in recent years as a target for domain-specific language design. The emergence of software-defined networking (SDN) as a popular paradigm for network programming has led to the appearance of a number of SDN programming languages seeking to provide high-level abstractions to simplify the task of specifying and reasoning about the packet-processing behavior of a network.

One success story has been the NetKAT family of languages. These are special-purpose languages and logics for specifying and reasoning about packet processing and network routing that fit well with the SDN paradigm. These languages provide general-purpose programming and logic constructs as well as special-purpose primitives for querying and modifying packet headers and encoding network topologies. Recent variants add probability and state. The most recent advance is a state-of-the-art implementation that scales to thousands of switches with good performance on standard benchmarks. Several practical applications of NetKAT have been developed, including algorithms for testing reachability, loop-freedom, and translation validation.

In contrast to competing approaches, NetKAT has always been based on a formal mathematical semantics, and the theoretical underpinnings have always been a first priority. There is an equational deductive system that is sound and complete, as well as a corresponding coalgebraic theory giving rise to an efficient bisimulation-based decision procedure. 

In this talk I will trace the evolution of this family of languages, focusing on the underlying theory and how it has been exploited to great practical effect.


 

Document Actions