It is our pleasure to present the proceedings volume of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), held from 9th to 12th July 2018 at Oxford (UK) as part of the Federated Logic Conference (FLoC 2018).

The Programme of LICS 2018 features invited talks by

• Thierry Coquand (University of Gothenburg), Univalent Type Theory,

• Javier Esparza (TU Mu¨nchen), Verification of Population Protocols,

• Ursula Martin (University of Oxford),On Diversity, and

• Val Tannen (University of Pennsylvania), Provenance Analysis for First-Order Model Checking,

in addition to the

• FLoC Plenary Lecture by Peter O’Hearn (University College London) on Continuous Reasoning for Big Code, and the

• FLoC Keynote Talk by Shafi Goldwasser (MIT) on Pseudo Deterministic Algorithms and Proofs.

Thierry Coquand, Javier Esparza, and Peter O’Hearn also contributed papers to this proceedings volume to accompany their invited talks. Further, this volume contains 92 contributed papers that were selected from 217 submissions. A total of 681 reviews were gathered for these submissions, and the selection of accepted papers was finalized following extensive discussions by the Programme Committee through the EasyChair conference management system. We would like to thank our fellow Programme Committee member for their hard work in selecting a high-quality programme for LICS 2018. We would also like to thank the 349 external reviewers and all authors who submitted papers for consideration.

Awards

This year the Kleene Award (sponsored by EATCS) for the Best Student Paper at LICS 2018, as judged by the Programme Committee, goes to

Etienne Miquey, A sequent calculus with dependent types for classical arithmetic.

To acknowledge the long-term foundational nature of papers appearing at LICS, a Test-of-Time Award is given annually to the paper or papers that were presented twenty years ago at LICS and that have “stood the test of time”. This year the Test-of-Time Award Committee consisting of of Christel Baier (chair), Luca Aceto, Anca Muscholl, and Vaughan Pratt selected the following two LICS 1998 papers for the 2018 LICS Test-of-Time award:

Samson Abramsky, Kohei Honda and Guy McCusker, A fully abstract game semantics for general references.

This paper presented the first games model of a programming language with higher-order store a la ML references. The result came as a big surprise within the community at the time and was a technical tour de force. Seen from today’s perspective, the article was certainly one of the main achievements of game semantics, and extended the reach of games models well beyond the work on PCF by Nickau, Hyland and Ong, and Abramsky, Jagadeesan and Malacaria (which received the 2017 Alonzo Church Award). The paper also opened a new field of research, which is still being explored and exploited today within the game-semantics community.

 

Martin Abadi, Cedric Fournet and Georges Gonthier, Secure Implementation of Channel Abstractions.

A secure channel is an important primitive in distributed systems programming. It protects the confidentiality of messages while they traverse untrusted networks. It is folklore that a secure channel can be implemented using cryptography, specifically using encryption. However, it is the LICS 1998 paper “Secure Implementation of Channel Abstractions” that formalizes this folklore idea and shows how to mathematically specify that a secure channel has been implemented correctly. In doing so, the paper also demonstrates, for the first time, how the classic concept of full abstraction of language translations can be used to formalize the preservation of security properties, an idea that has been used several times subsequently.

 

Finally, the Alonzo Church Award 2018 for Outstanding Contributions to Logic and Computation, given by SIGLOG, EATCS, EACSL, and the Kurt Gödel Society, was awarded at LICS 2018 jointly to Tomas Feder and Moshe Vardi for their fundamental contributions to the computational complexity of constant satisfaction problems, which appeared in the two papers

Thomas Feder and Moshe Y. Vardi, Monotone Monadic SNP and Constraint Satisfaction, STOC 1993, 612-622.

Thomas Feder and Moshe Y. Vardi, The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory. SIAM J. Comuting 28(1) (1998), 57-104.

The Feder-Vardi project aimed at finding a large subclass of NP that exhibits a dichotomy (all problems are either in PTIME or NP-complete). The approach is to find this subclass via syntactic prescriptions. The papers identified a class of problems specified by monotone monadic SNP without inequality, which they suggested might exhibit such a dichotomy. Feder and Vardi justified placing all three restrictions by showing, using Ladner's theorem, that classes obtained by dropping any one of the three restrictions do not have a dichotomy. They then explored the structure of this class. They show that all problems in this class reduce to the seemingly simpler class CSP – Constraint Satisfaction Problems. They divided CSP into subclasses and tried to unify the collection of all known polytime algorithms for CSP problems and extract properties that make CSP problems NP-hard. They conjectured that the class CSP (and therefore, also MMSNP) also satisfy the dichotomy property. This became known as the Feder-Vardi Dichotomy Conjecture. The Dichotomy Conjecture stimulated an extensive research program, which culminated in 2017 in two independent proofs, by A. Bulatov and by D. Zhuk, of its correctness.

We express our congratulations to all prize recipients.

 

Acknowledgements

We would like to thank all people that contributed to the success of LICS 2018. This includes in particular the organizers of the Federated Logic Conference FLoC 2018, headed by Marta Kwiatkowska, Daniel Kroening, and Moshe Vardi, the Steering Committee of LICS chaired by Martin Grohe, and the Publicity and Proceedings Chair Sam Staton.

 

Remembering Martin Hofmann

The preparation of LICS 2018 was overshadowed by the tragic death of its original PC Chair, Martin Hofmann, who died in January 2018 while hiking on Mount Nikko Shirane in Japan. Martin had already done an enormous amount of work in putting together the LICS programme. In particular, he had guided the composition of the Programme Committee and the selection of the invited speakers. After his untimely demise, Anuj Dawar and Erich Grädel took over the responsibility as PC Chairs for LICS. Martin Hofmann was a brilliant scientist and at the same time a friend and highly appreciated colleague. We missed him very much as we finalized the LICS programme and we shall miss him in the future. To honour Martin Hofmann a Memorial Session took place at LICS with a talk by Benjamin Pierce giving his personal reflections. In addition, there was a small symposium of the scientific work of Martin Hofmann at the LICS affiliated Workshop on Logic and Computation Complexity (LCC 2018) on the day after LICS. We hope that we have been able to present a volume of proceedings here that Martin would have been proud of, and we dedicate it to his memory.

 

 

 

 

---