The following two papers were selected from the Proceedings of LICS 2004 for the 2024 Test of Time Award. The committee consisted of Franz Baader (chair), Karoliina Lehtinen, Prakash Panangaden, and Albert Rubio.

Transition Invariants, by Andreas Podelski and Andrey Rybalchenko

The paper presents in a very clean and elegant way a general characterization of the validity of liveness properties of programs, like termination and other such properties expressed in temporal logic. This is achieved by employing relations over program states, called transition invariants, which contain the transitive closure of the state transition relation defined by the program. The key result is that the absence of infinite executions can be reduced to proving that the transition invariant is a finite union of well-founded relations. The authors show how to use such disjunctively well-founded transition invariants to validate temporal properties of concurrent systems. The paper has greatly influenced the development of techniques and tools for proving termination of programs automatically since it nicely combines the use of disjunctive well-foundedness with the construction of an abstraction of the program transition relation, which is the transition invariant. The suitability for automation of the approach has been crucial in its success. In addition, the paper also had a large impact on the design of powerful techniques based on termination analysis to (dis)prove a great variety of temporal properties of programs.

Preprint: [pdf]. DOI: [10.1109/LICS.2004.1319598].

A categorical semantics of quantum protocols, by Samson Abramsky and Bob Coecke

This extraordinary paper has had a major impact on the development of quantum computation in the logic and computation community. It has led to new algebraic and diagrammatic ways of thinking about quantum computation and has stimulated research on quantum programming languages, calculi for reasoning about quantum computation, and lately even error correction. Using the logic of compact closed categories, the paper gives an abstract treatment of fundamental aspects of quantum mechanics and quantum computation, with only sparse use of the usual mathematical machinery (such as linear algebra and Hilbert spaces). It shows that major protocols of quantum computation, such as teleportation and entanglement swapping, can not only be formulated, but also proved to be correct in this framework. Fundamental aspects of quantum mechanics are given an abstract treatment, most notably the Born rule. In summary, this paper began and gave impetus to the development of an abstract way to reason about quantum mechanics and quantum computation. It is very highly cited and has had major impact on reasoning about quantum computation and quantum mechanics.

Preprint: [arxiv:quant-ph/0402130 ]. DOI: [10.1109/LICS.2004.1319636].

LICS Sponsorship

The symposium is sponsored by ACM SIGLOG and the IEEE Technical Committee on Mathematical Foundations of Computing.