Symposium on Logic in Computer Science

Each year, since 2006, the LICS Test-of-Time Award recognizes those articles from LICS proceedings 20 years earlier, which have become influential.

• Leo Bachmair, Nachum Dershowitz, Jieh Hsiang, "Orderings for Equational Proofs"
• E. Allen Emerson, Chin-Laung Lei, "Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)"
• Moshe Y. Vardi, Pierre Wolper, "An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)"

• Samson Abramsky, "Domain theory in Logical Form"
• Robert Harper, Furio Honsell, Gordon D. Plotkin, "A Framework for Defining Logics"

• Martin Abadi, Leslie Lamport, "The existence of refinement mappings"

• Eugenio Moggi, "Computational lambda-calculus and monads"

• Rajeev Alur, Costas Courcoubetis, David L. Dill, "Model-checking for real-time systems"
• Jerry R. Burch, Edmund Clarke, Kenneth L. McMillan, David L. Dill, James Hwang, "Symbolic model checking: 10^20 states and beyond"
• Max Dauchet, Sophie Tison, "The theory of ground rewrite systems is decidable"
• Peter Freyd, "Recursive types reduced to inductive types"

• Patrice Godefroid, Pierre Wolper, "A partial approach to model checking"
• Joshua Hodas, Dale A. Miller, "Logic programming in a fragment of intuitionistic linear logic"
• Dexter Kozen, "A completeness theorem for Kleene algebras and the algebra of regular events"

• Thomas Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine, "Symbolic model checking for real-time systems"
• Jean-Pierre Talpin, Pierre Jouvelot, "The type and effect discipline"

• Leo Bachmair, Harald Ganzinger, Uwe Waldmann, "Set constraints are the monadic class"
• André Joyal, Mogens Nielson, Glynn Winskel, "Bisimulation and open maps"
• Benjamin C. Pierce, Davide Sangiorgi, "Typing and subtyping for mobile processes"

• Martin Hofmann, Thomas Streicher, "The groupoid model refutes uniqueness of identity proofs"
• Dale A. Miller, "A multiple-conclusion meta-logic"

• Igor Walukiewicz, "Completeness of Kozen's Axiomatisation of the Propositional Mu-Calculus"

• Parosh A. Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay, "General decidability theorems for infinite-state systems"
• Iliano Cervesato, Frank Pfenning, "A Linear Logical Framework"

• Richard Blute, Josée Desharnais, Abbas Edalat, Prakash Panangaden, "Bisimulation for Labelled Markov Processes"
• Daniele Turi, Gordon D. Plotkin, "Towards a Mathematical Operational Semantics"

• Martín Abadi, Cédric Fournet, Georges Gonthier, "Secure Implementation of Channel Abstractions"
• Samson Abramsky, Kohei Honda, Guy McCusker, "A Fully Abstract Game Semantics for General References"

• Marcelo P. Fiore, Gordon D. Plotkin, Daniele Turi, "Abstract Syntax and Variable Binding"
• Murdoch Gabbay, Andrew M. Pitts, "A New Approach to Abstract Syntax Involving Binders"

• Luca de Alfaro, Thomas A. Henzinger, "Concurrent Omega-Regular Games"
• Hiroshi Nakano, "A Modality for Recursion"

• Aaron Stump;, Clark W. Barrett, David L. Dill, Jeremy R. Levitt, "A Decision Procedure for an Extensional Theory of Arrays"
• Hongwei Xi, "Dependent Types for Program Termination Verification"

At each conference the Kleene award, in honour of S.C. Kleene, is given for the best student paper.