| Dexter Kozen |
| Thu 16 May 2019, 16:00 - 17:00 |
| Informatics Forum (IF-G.07) followed by G.02-Cafe |
If you have a question about this talk, please contact: Bob Fisher (rbf)
There will be a reception afterwards.
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 behaviour 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 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.
More details are here.