The 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation
The European Association for Computer Science Logic (EACSL), the European Association for Theoretical Computer Science (EATCS), and the ACM Special Interest Group for Logic and Computation (SIGLOG) are pleased to announce that the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to
Lars Birkedal, Aleš Bizjak, Derek Dreyer, Jacques-Henri Jourdan, Ralf Jung, Robbert Krebbers, Filip Sieczkowski, Kasper Svendsen, David Swasey and Aaron Turon
for the design and implementation of Iris, a higher-order concurrent separation logic framework.
The awardee papers are:
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer: “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning”. POPL 2015.
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ICFP 2016.
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. ESOP 2017.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).
Iris is a unifying framework that is at the same time rigorously founded and elegantly constructed, but also powerful and broadly applicable. Uniquely, Iris can explain a great variety of primitives in terms of a generic logic with a handful of well-understood mechanisms and comes with a mature implementation in the form of a Coq library. Iris has been very influential and has been applied for reasoning about a diverse range of systems, including fine-grained concurrency, weak memory, various type systems (recursive types, ownership types, gradual types, session types etc.), assembly languages, object capabilities, probabilistic languages, distributed systems and last but not least, models of practical languages like Rust, Scala and OCaml. Its features like higher-order ghost state, atomic invariants, guarded recursion have been used to implement program logics for partial and total correctness, but also unary and relational logical relations, and have in many cases made it possible to significantly advance the state of the art for applying those techniques. In addition to the development of Iris itself, Iris is at the core of a vibrant community. The Coq implementation is developed as open source software with regular releases. Course material has been developed, live tutorials have been taught and two dedicated Iris Workshops have been organised.
The 2022 Alonzo Church Award for Outstanding Contributions to Logic and Computation
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 Gödel Society (KGS) are pleased to announce that the 2022 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given to
Dexter Kozen
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)
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 variety of problems over the past 25 years, including modeling and reasoning about packet-switched networks.
The 2021 Alonzo Church Award for Outstanding Contributions to Logic and Computation
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 Gödel Society (KGS) are pleased to announce that
Georg Gottlob, Christoph Koch, Reinhard Pichler, Klaus U. Schulz, and Luc Segoufin
have been selected as the winners of the 2021 Alonzo Church Award for
fundamental work on logic-based web data extraction and querying tree-structured data,
published in:
(1) Georg Gottlob and Christoph Koch. “Monadic Datalog and the Expressive Power of Languages for Web Information Extraction.” Journal of the ACM (JACM) 51.1 (2004): 74-113.
(2) Georg Gottlob, Christoph Koch, and Klaus U. Schulz. “Conjunctive Queries Over Trees.” Journal of the ACM (JACM) 53.2 (2006): 238-272.
(3) Georg Gottlob, Christoph Koch, and Reinhard Pichler. “Efficient Algorithms for Processing XPath Queries.” ACM Transactions on Database Systems (TODS) 30.2 (2005): 444-491.
(4) Georg Gottlob, Christoph Koch, Reinhard Pichler, and Luc Segoufin. “The Complexity of XPath Query Evaluation and XML Typing.” Journal of the ACM (JACM) 52.2 (2005): 284-335.
THE CONTRIBUTION
Paper (1) establishes a comprehensive logical theory of Web data extraction. At its core, this is the problem of selecting relevant nodes (subtrees) from HTML text. While the set of relevant nodes can be expressed in Monadic Second-Order logic (MSO) over finite trees, MSO has high computationally complexity. The authors prove that Monadic Datalog on trees has exactly the same expressive power as full MSO and that, surprisingly, evaluating Monadic Datalog is feasible in time linear in the size of query and input tree. These results greatly influenced theoretical and applied research, and gave rise to logic-based systems for data extraction that have been successfully used in industry.
Papers (2,3,4) present deep investigations into logical queries over tree-structured
data. The complexity of evaluating XPath, a key technology in Web browsers and other systems, was unclear, and available implementations required exponential time. Paper (2) gives a full characterization of, and a dichotomy theorem for, the complexity of conjunctive queries on various representations of trees. Paper (3) shows that the full XPath standard can be evaluated in PTIME and proposes a logical core which has become seminal to research efforts at the intersection of Web data processing and (modal) logics. Finally, paper (4) establishes the precise complexity of evaluating XPath fragments.
The 2020 Alonzo Church Award for Outstanding Contributions to Logic and Computation
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 Gödel Society (KGS) are pleased to announce that
Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, Lucian Popa, and Wang Chiew Tan
have been selected as the winners of the 2020 Alonzo Church Award for Outstanding Contributions to Logic and Computation. The award recognizes their ground-breaking work on laying the logical foundations for data exchange, described in the following papers:
(1) Ronald Fagin, Phokion G. Kolaitis, Lucian Popa, Renée J. Miller. Data exchange: Semantics and Query Answering, Proceedings of the 9th International Conference on Database Theory (ICDT 2003), pp. 207-223, 2003.
Full journal version: Theoretical Computer Science, Vol. 336, No. 1, pp. 89-124, 2005.
(2) Ronald Fagin, Phokion G. Kolaitis, Lucian Popa, Wang Chiew Tan. Composing Schema Mappings: Second-Order Dependencies to the Rescue, Proceedings of the 23rd ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 2004), pp. 83-94, 2004.
Full journal version: ACM Transactions on Database Systems, Vol. 30, No. 4, pp. 994-1055, 2005.
Data exchange is the problem of transforming data structured under a schema, called the source schema, into data conforming to a different schema, called the target schema. The results and techniques developed have in addition to gaining theoretical insights influenced the development of industrial and academic tools. The 2020 Church Award was selected by a panel consisting of Mariangiola Dezani, Thomas Eiter (chair), Javier Esparza, Radha Jagadeesan and Natarajan Shankar.
THE CONTRIBUTION
Data exchange is an old and ubiquitous problem in data management that was described by Philip Bernstein as the “oldest problem in databases”. Early work on data exchange used low-level, ad hoc programs to transform data from the source schema to the target schema, which resulted into inefficiencies and limited reusability. Publications (1) and (2) laid the logical foundations for data exchange and became the catalyst for the development of data exchange as a research area in its own right. Publication (1) is about logic in computer science: a fragment of first-order logic, called source-to-target tuple-generating dependencies (in short, s-t tgds), is systematically used as a specification language in data exchange. The algorithmic and structural properties of s-t tgds are explored, and the concept of a universal solution is introduced as the preferred way to carry out the data exchange task. Publication (2) is about logic from computer science: first, it is shown that the language of s-t tgds is not closed under composition; second, a new fragment of second-order logic, called second-order tuple-generating dependencies (in short, SO tgds) is identified and shown to be the “right” logic-based specification language for composing s-t tgds. The award publications are well-cited and have been recognized with two test-of-time awards.
The 2019 Alonzo Church Award for Outstanding Contributions to
Logic and Computation
The 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations.
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 Gödel Society (KGS) are pleased to announce that Murdoch J. Gabbay (Heriot-Watt University, UK) and Andrew M. Pitts (Cambridge University, UK) have been selected as the winners of the 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation. The award recognizes their ground-breaking work introducing the theory of nominal representations, a powerful and elegant mathematical model for computing with data involving atomic names, described in the following papers:
- Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13(3):341– 363, 2002.
- Andrew M. Pitts. Nominal logic, a first order theory of names and binding, Information and Computation 186(2):165–193, 2003.
For the invention of nominal techniques, providing a highly in- fluential mathematical model for key concepts that arise when computing with data involving atomic names.
The 2019 Church Award was selected by a panel consisting of Thomas Eiter, Javier Esparza, Radha Jagadeesan, Catuscia Palamidessi, and Natarajan Shankar.
Description of the contribution
The 2018 Alonzo Church Award for Outstanding Contributions to
Logic and Computation
The 2018 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to Tomas Feder and Moshe Y. Vardi for fundamental contributions to the computational complexity of constraint-satisfaction problems. Their contributions appeared in two papers:
1. Tomas Feder, Moshe Y. Vardi: Monotone Monadic SNP and Constraint Satisfaction. STOC 1993, 612-622.
2. Tomas Feder, Moshe Y. Vardi: The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory. SIAM J. Comput. 28(1), 57–104 (1998).
CONTRIBUTION SUMMARY: The Feder-Vardi project aimed at finding a large subclass of NP that exhibits a dichotomy (all problems are either in PTIME or NP-complete). The approach is to find this subclass via syntactic prescriptions. The paper identified a class of problems specified by “monotone monadic SNP without inequality”, which may exhibit this dichotomy. Feder and Vardi justified placing all three restrictions by showing, using Lad- ner’s theorem, that classes obtained by using only two of the above three restrictions do not show this dichotomy. They then explored the structure of this class. They show that all problems in this class reduce to the seemingly simpler class CSP – Constraint Satisfaction Problems. They divided CSP into subclasses and tried to unify the collection of all known polytime algorithms for CSP problems and extract properties that make CSP problems NP-hard. They conjectured that the class CSP (and therefore, also MMSNP) also satisfy the dichotomy property. This became known as the Feder-Vardi Dichotomy Conjecture. The Dichotomy Conjecture stimulated an exten- sive research program, which culminated in 2017 in two independent proofs, by A. Bulatov and by D. Zhuk, of its correctness.
Description of the contribution
The 2017 Alonzo Church Award for Outstanding Contributions to
Logic and Computation
The 2017 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria,
Martin Hyland, Luke Ong, and Hanno Nickau for providing a fully-abstract semantics for higher-order computation through the introduction of game models, thereby fundamentally revolutionising the field of programming language semantics, and for the applied impact of these models.
Description of the contribution
The 2016 Alonzo Church Award for Outstanding Contributions to
Logic and Computation
The 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given to Rajeev Alur and David Dill for their invention of timed automata, a decidable model of real-time systems, which combines a novel, elegant, deep theory with widespread practical impact.