[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
2022 ALONZO CHURCH AWARD ANNOUNCEMENT
The ACM Special Interest Group on Logic (SIGLOG), the European Association for
Theoretical Computer Science (EATCS), the European Association for Computer
Science Logic (EACSL), and the Kurt Goedel Society (KGS) are pleased to
announce that
Dexter Kozen
has been selected as the winner of the
2022 Alonzo Church Award for Outstanding Contributions to Logic and
Computation
for his fundamental work on developing the theory and applications of Kleene
Algebra with Tests, an equational system for reasoning about iterative
programs, published in:
Kleene Algebra with Tests. ACM Transactions on Programming Languages and
Systems 19(3): 427-443 (1997).
THE CONTRIBUTION
This work on Kleene Algebra with Tests (KAT) is one of the high points among
remarkable contributions of Dexter Kozen to logics of programs. It is a
culmination of a series of articles by Dexter Kozen that define and apply
Kleene Algebra with Tests (KAT), an equational system that combines Kleene
Algebra (the algebra of regular expressions) with Boolean Algebra (the tests).
Together, the terms of the two algebras are capable of representing while
programs, and their combined equational theory is capable of proving a wide
range of important properties of programs. Although reasoning in KAT under
arbitrary commuting conditions is undecidable, Kozen observes that when the
commuting conditions are limited to including tests, it is decidable and in
PSPACE. He illustrates the power of KAT with these decidable commuting
conditions by proving a well-known folk theorem: Every while program can be
simulated by a program with just one loop. KAT has been successfully applied to
a variet!
y of problems over the past 25 years, including modeling and reasoning about
packet-switched networks.
The 2022 Church Award was selected by a jury consisting of Thomas Colcombet,
Mariangiola Dezani, Javier Esparza, Radha Jagadeesan (chair), and Igor
Walukiewicz.
