The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual

academic conference An academic conference or scientific conference (also congress, symposium, workshop, or meeting) is an Convention (meeting), event for researchers (not necessarily academics) to present and discuss their scholarly work. Together with academic jou ...

on the theory and practice of

computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

in relation to

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

History

LICS was originally sponsored solely by the

IEEE The Institute of Electrical and Electronics Engineers (IEEE) is an American 501(c)(3) organization, 501(c)(3) public charity professional organization for electrical engineering, electronics engineering, and other related disciplines. The IEEE ...

, but as of the 2014 founding of the ACM Special Interest Group on Logic and Computation LICS has become the flagship conference of SIGLOG, under the joint sponsorship of ACM and IEEE. From the third installment in 1988 until 2013, the cover page of the conference proceedings has featured an artwork entitled ''Irrational Tiling by Logical Quantifiers'', by

Alvy Ray Smith Alvy Ray Smith III (born September 8, 1943) is an American computer scientist who co-founded Lucasfilm's Computer Division and Pixar, participating in the 1980s and 1990s expansion of computer animation into feature film. He is one of the 50 F ...

. Since 1995, each year the '' Kleene award'' is given to the best student paper. In addition, since 2006, the ''LICS Test-of-Time Award'' is given annually to one among the twenty-year-old LICS papers that have best met the test of time.LICS awards website
/ref>

LICS Awards

Test-of-Time Award

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

2006

* Leo Bachmair,

Nachum Dershowitz Nachum Dershowitz () is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the Path_ordering_(term_rewriting), multiset path ordering used to prove Rewriting#Termination, termination of term rewrite systems. Educat ...

, 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)"

2007

Samson Abramsky Samson Abramsky (born 12 March 1953) is a British computer scientist who is a Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 t ...

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

2008

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

2009

Eugenio Moggi Eugenio Moggi is a professor of computer science at the University of Genoa, Italy. He first described the general use of monads to structure programs. Biography Academic qualifications: * PhD in Computer Science, University of Edinburgh ...

, "Computational lambda-calculus and monads"

2010

* 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 Peter John Freyd (; born February 5, 1936) is an American mathematician, a professor at the University of Pennsylvania, known for work in category theory and for founding the False Memory Syndrome Foundation. Mathematics Freyd obtained his Ph ...

, "Recursive types reduced to inductive types"

2011

* Patrice Godefroid, Pierre Wolper, "A partial approach to model checking" * Joshua Hodas, Dale Miller, "Logic programming in a fragment of intuitionistic linear logic" *

Dexter Kozen Dexter Campbell Kozen (born December 20, 1951) is an American theoretical computer scientist. He is Professor Emeritus and Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. Career Kozen received his BA in mathematics from ...

, "A completeness theorem for Kleene algebras and the algebra of regular events"

2012

* 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"

2013

* Leo Bachmair,

Harald Ganzinger Harald Ganzinger (31 October 1950, Werneck – 3 June 2004, Saarbrücken) was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state-of-the-art automated ...

, Uwe Waldmann, "Set constraints are the monadic class" *

André Joyal André Joyal (; born 1943) is a professor of mathematics at the Université du Québec à Montréal who works on category theory. He was a member of the School of Mathematics at the Institute for Advanced Study in 2013, where he was invited to jo ...

, Mogens Nielson, Glynn Winskel, "Bisimulation and open maps" * Benjamin C. Pierce, Davide Sangiorgi, "Typing and subtyping for mobile processes"

2014

Thomas Streicher Thomas Streicher (11 February 1958 – 2 January 2025) was an Austrian mathematician who was a Professor of Mathematics at Technische Universität Darmstadt. He received his PhD in 1988 from the University of Passau with advisor Manfred Broy. L ...

, "The groupoid model refutes uniqueness of identity proofs" * Dale Miller, "A multiple-conclusion meta-logic"

2015

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

2016

* Parosh A. Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay, "General decidability theorems for infinite-state systems" * Iliano Cervesato,

Frank Pfenning Frank Pfenning is a German-American professor of computer science, adjunct professor in philosophy, and was head of the Computer Science Department at Carnegie Mellon University from 2013 to 2018. Education and career Pfenning grew up in Rüsse ...

, "A Linear Logical Framework"

2017

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

2018

* Martín Abadi, Cédric Fournet, Georges Gonthier, "Secure Implementation of Channel Abstractions" *

, Kohei Honda, Guy McCusker, "A Fully Abstract Game Semantics for General References"

2019

* 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"

2020

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

2021

* 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"

Kleene award

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

Notes

External links

LICS home page
{{Authority control Theoretical computer science conferences Logic conferences Logic in computer science IEEE conferences