Dexter Kozen, the Joseph Newton Pew, Jr. Professor of Engineering, and member of the Cornell Computer Science faculty since 1984, delivered the Milner Lecture at the University of Edinburgh, Scotland. Kozen addressed the Laboratory for Foundations of Computer Science (LFCS) on the topic “Software Defined Networks and the NetKAT Family of Languages.” As Kozen explains it, in this talk, he “trace[s] the evolution of this family of languages, focusing on the underlying theory and how it has been exploited to great practical effect.”
Kozen says that “[n]etworks 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.” Kozen then highlights the NetKAT family of languages, which he describes as a “success story”:
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.
Moreover, Kozen continues, “[i]n 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.”
Kozen, whose relationship with Cornell CS goes back to his doctoral studies, when he worked under the direction of department founder, Juris Hartmanis, is the author, most recently, of Theory of Computation and many articles on programming languages, networks, security, and theory of computing; co-author of Dynamic Logic; and the recipient of numerous teaching awards.
Founded in 1987, the Laboratory for Foundations of Computer Science (LFCS) is one of seven research institutes in the School of Informatics at the University of Edinburgh. It is described as a “community of theoretical computer scientists with interests in concurrency, semantics, categories, algebra, types, logic, algorithms, complexity, databases and modelling,” whose research agenda is “the study of theories which underlie, or should in future underlie, the analysis and design of computing systems.”
In recent decades, the Milner Lecture has been given by fellow CS faculty, including Éva Tardos (2013) and Joseph Halpern (2000).