Symposium on Logic in Computer Science: Difference between revisions

Revision as of 09:05, 14 August 2020

Latest revision as of 09:18, 2 July 2025

(11 intermediate revisions by 11 users not shown)

Line 1:

{{Short description|Computer science and logic conference}}

{{dablinkHatnote|For the article on the topic of logic in computer science, see [[logic in computer science]].}}

{{More citations needed|date=July 2020}}

The '''ACM–IEEE Symposium on Logic in Computer Science''' ('''LICS''') is an annual [[academic conference]] on the theory and practice of [[computer science]] in relation to [[mathematical logic]]. 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]], but as of the 2014 founding of the [[ACM SIGLOG|ACM Special Interest Group on Logic and Computation]] LICS has become the flagship conference of SIGLOG, under the joint sponsorship of ACM and IEEE.<ref>{{citation|title=Welcome to SIGLOG!|department=Chair's Letter|journal=SIGLOG News|volume=1|issue=1|date=July 2014|pages=2–3|url=http://siglog.hosting.acm.org/?attachment_id=71|first=Prakash|last=Panangaden|authorlinkauthor-link=Prakash Panangaden}}.</ref>

From the third

Since the first installment in 1988, the cover page of the conference proceedings has featured an artwork entitled ''Irrational Tiling by Logical Quantifiers'', by [[Alvy Ray Smith]].<ref>[http://www.alvyray.com/Art/Irrational.htm Irrational Tiling by Logical Quantifiers] LICS cover by Alvy Ray Smith.</ref>

<ref>{{cite web |title=LICS archive |url=http://lics.siglog.org/archive/conferences.html |website=ACM/IEEE Symposium on Logic in Computer Science |access-date=26 February 2024}}</ref>

Since the first 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]].<ref>[http://www.alvyray.com/Art/Irrational.htm Irrational Tiling by Logical Quantifiers] LICS cover by Alvy Ray Smith.</ref>

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.<ref>[http://lics.rwth-aachen.de/awards.html LICS awards website]</ref>

Line 15 ⟶ 18:

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

==== 2020 ====

==== 20202006 ====

* [[Luca de Alfaro]], [[Thomas A. Henzinger]], "Concurent Omega-Regular Games"

*[[Leo Bachmair]], [[Nachum Dershowitz]], [[Jieh Hsiang]], "Orderings for Equational Proofs"

* [[Hiroshi Nakano]], "A Modality for Recursion"

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

==== 20192007 ====

*[[Samson Abramsky]], "Domain theory in Logical Form"

*[[Robert Harper (computer scientist)|Robert Harper]], [[Furio Honsell]], [[Gordon D. Plotkin]], "A Framework for Defining Logics"

==== 20132008 ====

* [[Marcelo P. Fiore]], [[Gordon D. Plotkin]], [[Daniele Turi]], "Abstract Syntax and Variable Binding"

* [[MurdochMartin GabbayAbadi]], [[AndrewLeslie M. PittsLamport]], "A New Approach toThe Abstractexistence Syntaxof Involvingrefinement Bindersmappings"

==== 20182009 ====

*[[Eugenio Moggi]], "Computational lambda-calculus and monads"

==== 20112010 ====

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

* [[SamsonRajeev AbramskyAlur]], [[KoheiCostas HondaCourcoubetis]], [[GuyDavid McCuskerL. Dill]], "A Fully Abstract Game SemanticsModel-checking for Generalreal-time Referencessystems"

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

==== 20172011 ====

*[[Patrice Godefroid]], [[Pierre Wolper]], "A partial approach to model checking"

*[[Joshua Hodas]], [[Dale A.Miller (academic)|Dale Miller]], "Logic programming in a fragment of intuitionistic linear logic"

*[[Dexter Kozen]], "A completeness theorem for Kleene algebras and the algebra of regular events"

==== 20092012 ====

* [[Richard Blute ]], [[Josée Desharnais]], [[Abbas Edalat]], [[Prakash Panangaden]], "Bisimulation for Labelled Markov Processes"

*[[Thomas Henzinger]], [[Xavier Nicollin]], [[Joseph Sifakis]], [[Sergio Yovine]], "Symbolic model checking for real-time systems"

* [[Daniele Turi]], [[Gordon D. Plotkin]], "Towards a Mathematical Operational Semantics"

*[[Jean-Pierre Talpin]], [[Pierre Jouvelot]], "The type and effect discipline"

==== 20162013 ====

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

==== 20072014 ====

* [[Parosh A. Abdulla]], [[Karlis Cerans]], [[Bengt Jonsson (computer scientist)|Bengt Jonsson]], [[Yih-Kuen Tsay]], "General decidability theorems for infinite-state systems"

*[[{{ill|Martin Hofmann]] (computer scientist)|lt=Martin Hofmann|de|Martin Hofmann (Informatiker)}}, [[Thomas Streicher]], "The groupoid model refutes uniqueness of identity proofs"

* [[Iliano Cervesato]], [[Frank Pfenning]], "A Linear Logical Framework"

*[[Dale A.Miller (academic)|Dale Miller]], "A multiple-conclusion meta-logic"

==== 2015 ====

Line 44 ⟶ 62:

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

==== 20142016 ====

*[[Martin Hofmann]], [[Thomas Streicher]], "The groupoid model refutes uniqueness of identity proofs"

*[[Dale A. Miller]], "A multiple-conclusion meta-logic"

* [[Parosh A. Abdulla]], [[Karlis Cerans]], [[Bengt Jonsson (computer scientist)|Bengt Jonsson]], [[Yih-Kuen Tsay]], "General decidability theorems for infinite-state systems"

==== 2013 ====

* [[Iliano Cervesato]], [[Frank Pfenning]], "A Linear Logical Framework"

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

==== 20122017 ====

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

* [[Richard Blute ]], [[Josée Desharnais]], [[Abbas Edalat]], [[Prakash Panangaden]], "Bisimulation for Labelled Markov Processes"

==== 2011 ====

* [[PatriceDaniele GodefroidTuri]], [[PierreGordon WolperD. Plotkin]], "A partialTowards approacha toMathematical modelOperational checkingSemantics"

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

==== 20102018 ====

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

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

==== 2009 ====

* [[Samson Abramsky]], [[Kohei Honda]], [[Guy McCusker]], "A Fully Abstract Game Semantics for General References"

*[[Eugenio Moggi]], "Computational lambda-calculus and monads"

==== 20082019 ====

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

* [[Marcelo P. Fiore]], [[Gordon D. Plotkin]], [[Daniele Turi]], "Abstract Syntax and Variable Binding"

==== 2007 ====

* [[Murdoch Gabbay]], [[Andrew M. Pitts]], "A New Approach to Abstract Syntax Involving Binders"

*[[Samson Abramsky]], "Domain theory in Logical Form"

*[[Robert Harper]], [[Furio Honsell]], [[Gordon D. Plotkin]], "A Framework for Defining Logics"

==== 20062020 ====

*[[Leo Bachmair]], [[Nachum Dershowitz]], [[Jieh Hsiang]], "Orderings for Equational Proofs"

* [[Luca de Alfaro]], [[Thomas A. Henzinger]], "ConcurentConcurrent Omega-Regular Games"

*[[E. Allen Emerson]], [[Chin-Laung Lei]], "Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)"

* [[Hiroshi Nakano (computer scientist)|Hiroshi Nakano]], "A Modality for Recursion"

*[[Moshe Y. Vardi]], [[Pierre Wolper]], "An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)"

==== 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 ===

Line 91 ⟶ 99:

==Notes==

{{reflistReflist}}

== External links ==

* [http://lics.siglog.org/ LICS home page]

{{IEEE conferences}}

{{Authority control}}

[[Category:Theoretical computer science conferences]]

[[Category:Logic conferences]]