Assistant Professor Justin Hsu and his coauthors have been awarded a distinguished paper award at POPL 2020 (ACM SIGPLAN Symposium on the Principles of Programming Languages). Hsu’s coauthors are Steffen Smolka (Cornell University), Nate Foster (Cornell University), Tobias Kappé (University College London), Dexter Kozen (Cornell University), and Alexandra Silva (University College London).
Hsu’s paper is entitled “Guarded Kleene Algebra with Tests.” Hsu explains, “Kleene Algebra with Tests (KAT) is a classical method for showing that two programs are equivalent, or showing that a program conforms to a specification.” KAT can model a variety of common program constructs—sequencing, conditionals, loops, etc.—but it is designed to accommodate programs that can make non-deterministic choices, according to Hsu. This work proposes Guarded KAT, a version of KAT with only deterministic choice. While the language is more restricted, GKAT is expressive enough to model typical programs. Furthermore, deciding equivalence for GKAT can be exponentially faster than deciding equivalence for KAT.
POPL is one of the flagship conferences for research on programming languages and formal verification. The 2020 conference takes place January 19-25 in New Orleans.