Thu 16 Jun 2022 16:10 - 16:30 at Kon-Tiki - Semantics Chair(s): Nate Foster
Fri 17 Jun 2022 04:10 - 04:30 at Kon-Tiki - Semantics

Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert’s task. Abstruse metatheory is holding back KAT’s potential.

We offer a fast path to a ``minimum viable model'' of a KAT, formally or in code through our framework, \textit{Kleene algebra modulo theories} (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT’s semantics, prove its equational theory sound and complete with respect to a tracing semantics, and derive a normalization-based decision procedure for equivalence checking. Our framework is based on \textit{pushback}, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over \emph{unbounded state}, reasoning about monotonically increasing, unbounded natural numbers. We provide an OCaml implementation that closely matches the theory: users can define and compose KATs with the ML module system.

Thu 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

15:30 - 16:50
SemanticsPLDI at Kon-Tiki +12h
Chair(s): Nate Foster Cornell University
15:30
20m
Talk
A Typed Continuation-Passing Translation for Lexical Effect Handlers
PLDI
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen
DOI
15:50
20m
Talk
Deep and Shallow Types for Gradual Languages
PLDI
Ben Greenman Brown University
DOI
16:10
20m
Talk
Kleene Algebra Modulo Theories: A Framework for Concrete KATs
PLDI
Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University
DOI Pre-print
16:30
20m
Talk
Semantic Soundness for Language Interoperability
PLDI
Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA)
DOI

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

03:30 - 04:50
SemanticsPLDI at Kon-Tiki
03:30
20m
Talk
A Typed Continuation-Passing Translation for Lexical Effect Handlers
PLDI
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tuebingen
DOI
03:50
20m
Talk
Deep and Shallow Types for Gradual Languages
PLDI
Ben Greenman Brown University
DOI
04:10
20m
Talk
Kleene Algebra Modulo Theories: A Framework for Concrete KATs
PLDI
Michael Greenberg Stevens Institute of Technology, Ryan Beckett Microsoft Research, USA, Eric Campbell Cornell University
DOI Pre-print
04:30
20m
Talk
Semantic Soundness for Language Interoperability
PLDI
Daniel Patterson Northeastern University, Noble Mushtak Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University (USA)
DOI