# ACM-IEEE Symposium on Logic in Computer Science

La conférence ACM-IEEE Symposium on Logic in Computer Science (abrégé en LICS) est la principale conférence scientifique informatique en relation avec la logique mathématique. Elle a lieu annuellement, sous les auspices du Special Interest Group on Logic and Computation (SIGLOG) et est organisée par l'ACM et le IEEE.

## Organisation
### Sélection et actes

Comme c'est le cas pour la plupart des conférences en informatique théorique, les contributions proposées sont évaluées au préalable par des pairs. Le taux d'acceptation est nettement inférieur à 50 %. Pour 2016, il y a eu 85 articles acceptés parmi les 191 soumissions. Pour la sélection, 577 avis de pairs ont été obtenus de 264 rapporteurs. Les articles retenus sont publiés dans les actes du colloque, éditées conjointement par l'ACM et l'IEEE. Des versions détaillées d'articles retenus paraissent fréquemment dans des revues de renom comme Logical Methods in Computer Science ou ACM Transactions on Computational Logic

### Historique

Au départ, LICS était financée seulement par la IEEE ; depuis 2014 LICS est devenu l'événement phare du ACM Special Interest Group on Logic and Computation (SIGLOG|) et est patronnée en commun par l'ACM et la IEEE.
Depuis la première conférence en 1988, la page de couverture des actes du colloque est décorée d'un dessin intitulé Irrational Tiling by Logical Quantifiers, par Alvy Ray Smith.

### Thèmes

Les sujets de la conférence comprennent notamment : Théorie des automates, déduction automatique, modèles et logiques catégoriques, concurrence et calcul distribué, programmation par contraintes, mathématiques constructives, théorie des bases de données, procédures de décision, logiques de description, théorie des domaines, théorie des modèles finis, aspects logiques de la bio-informatique, aspects logiques de la complexité des calculs, aspects logiques du calcul quantique, logiques de programmes, logiques modales et temporelles, vérification de modèles, systèmes probabilistes, calculs de processus, langages de programmation sémantiques.

### Localisation

Les lieux de la conférence varient : la première conférence, en 1986, a eu lieu à Cambridge (Massachusetts) ; LICS 2014 à Vienne, LICS 2015 à Kyoto, Japon, LICS 2016 à Columbia University à New York City et LICS 2017 à Reykjavik.
Plusieurs Workshop ont lieu en même temps que la conférence. Pour la conférence de 2016, il y avait 5 workshops :
* Logic Mentoring Workshop
* LSB: Workshop on Logic and Systems Biology
* NLCS: Workshop on Natural Language and Computer Science
* SR: International Workshop on Strategic Reasoning
* LOLA: Syntax and Semantics of Low-Level Languages

## Prix LICS

Deux prix sont décernés à chaque session, le prix du meilleur article d'étudiant (prix Kleene) et le prix du meilleur article de plus de 20 ans (test-of-time). C'est un comité de sélection spécial qui attribue ces récompenses.

### prix Kleene

Chaque année depuis 1995, un Kleene award (en) est décerné au meilleur article d'étudiant, nommé ainsi en l'honneur de Stephen Cole Kleene. Lauréats récents :

#### 2016

* Steen Vester, « Winning cores in parity games »

#### 2015

* Fabian Reiter, « Distributed Graph Automata »

#### 2014

* Flavien Breuvart, « On the characterization of models of H »
* Yaron Velner, « Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives »

### prix Test-of-Time

Chaque année depuis 2006, le prix LICS Test-of-Time Award est remis en reconnaissance des articles parus dans les actes de colloques au moins 20 ans plus tôt et qui continuent à avoir une influence.

#### 2017

* Amina Doumane - « On the infinitary proof theory of logics with fixed points »

#### 2016

* Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsa, « General Decidability Theorems for Infinite-State Systems »
* Iliano Cervesato, Frank Pfenning, « A Linear Logical Framework »

#### 2015

* Igor Walukiewicz, « Completeness of Kozen’s Axiomatisation of the Propositional μ-Calculus »

#### 2014

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

#### 2013

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

#### 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 »

#### 2011

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

#### 2010

* Rajeev Alur, Costas Courcoubetis, David L. Dill, « Model-checking for real-time systems »
* Jerry R. Burch, Edmund M. 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 »

#### 2009

* Eugenio Moggi, « Computational lambda-calculus and monads »

#### 2008

* Martín Abadi, Leslie Lamport, « The existence of refinement mappings »

#### 2007

* Samson Abramsky, « Domain theory in Logical Form »