Symposium om logik i datavetenskap
ACM –IEEE Symposium on Logic in Computer Science ( LICS ) är en årlig akademisk konferens om datavetenskapens teori och praktik i relation till matematisk logik . Utökade versioner av utvalda artiklar från varje års konferens visas i kända internationella tidskrifter som Logical Methods in Computer Science och ACM Transactions on Computational Logic .
Historia
LICS sponsrades ursprungligen enbart av IEEE , men från och med grundandet 2014 av ACM Special Interest Group on Logic and Computation har LICS blivit flaggskeppskonferensen för SIGLOG, under gemensam sponsring av ACM och IEEE.
Från den första delen 1988 fram till 2013 har försättsbladet till konferenshandlingarna innehållit ett konstverk med titeln Irrational Tiling av Logical Quantifiers, av Alvy Ray Smith .
delas Kleene-priset varje år ut till den bästa studentuppsatsen. Sedan 2006 delas dessutom LICS Test-of-Time Award ut årligen till en av de tjugo år gamla LICS-uppsatser som bäst klarat tidens tand.
LICS Awards
Test-of-Time Award
Varje år, sedan 2006, erkänner LICS Test-of-Time Award de artiklar från LICS-processer 20 år tidigare, som har blivit inflytelserika.
2006
- Leo Bachmair, Nachum Dershowitz , Jieh Hsiang, "Orderingar för ekvationella bevis"
- 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 , "Domänteori i logisk form"
- Robert Harper , Furio Honsell, Gordon D. Plotkin , "A Framework for Defining Logics"
2008
- Martin Abadi , Leslie Lamport , "Existensen av förfiningskartläggningar"
2009
- Eugenio Moggi , "Computational lambda-kalkyl och monader"
2010
- Rajeev Alur , Costas Courcoubetis, David L. Dill , "Modelkontroll för realtidssystem"
- 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, "Teorin om system för omskrivning av mark kan avgöras"
- Peter Freyd , "Rekursiva typer reducerade till induktiva typer"
2011
- Patrice Godefroid, Pierre Wolper , "A partial approach to model checking"
- Joshua Hodas, Dale A. Miller, "Logikprogrammering i ett fragment av intuitionistisk linjär logik"
- Dexter Kozen , "En fullständighetsteorem för Kleene algebror och algebra för vanliga händelser"
2012
- Thomas Henzinger , Xavier Nicollin, Joseph Sifakis , Sergio Yovine, "Symbolisk modellkontroll för realtidssystem"
- Jean-Pierre Talpin, Pierre Jouvelot, "Typ- och effektdisciplinen"
2013
- Leo Bachmair, Harald Ganzinger , Uwe Waldmann, "Setliga begränsningar är den monadiska klassen"
- André Joyal , Mogens Nielson, Glynn Winskel, "Bisimulering och öppna kartor"
- Benjamin C. Pierce , Davide Sangiorgi , "Skrivning och subtypning för mobila processer"
2014
- Martin Hofmann, Thomas Streicher , "Groupoidmodellen motbevisar det unika med identitetsbevis"
- Dale A. Miller, "En metalogik med flera slutsatser"
2015
- Igor Walukiewicz, "Fullständigheten av Kozens axiomatisering av den propositionella Mu-Calculus"
2016
- 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"
2017
- Richard Blute, Josée Desharnais, Abbas Edalat , Prakash Panangaden , "Bisimulation for Labeled 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"
- Samson Abramsky , 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, "beroende typer för verifiering av programavslutning"
Kleene utmärkelse
Vid varje konferens delas Kleene-priset , för att hedra SC Kleene , för bästa studentuppsats.
Se även
- Listan över datavetenskapskonferenser innehåller andra akademiska konferenser inom datavetenskap.