Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL).
It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
CSL'22 will be held online on February 14 - 19, 2022. The event is hosted by the University of Göttingen.
To register for CSL 2022, please fill in the registration form here.
The participation fee for CSL is as follows:
- members of EACSL (2022): free
- students: 5 Euro
- members of EATCS or ACM SIGLOG (2022): 15 Euro
- regular: 20 Euro
This fee covers participation in CSL and includes membership of EACSL for 2022. This fee has to be paid directly to the EACSL, as indicated in the registration process, and is processed by the EACSL.
Speaker registration deadline: January 31st, 2022. At least one author of every contributed paper must register as a speaker.
Non-speaker registration deadline: February 6th, 2022. All participants must register.
There is no participation fee for the collocated workshops. As such, to participate in the workshops, one does not need to pay the registration fee for CSL, but the registration form should still be filled.
These participation fees are made possible only due to the generous financial support by the German Research Foundation (DFG) and the University of Göttingen.
Tuesday: 10:00 - 11:00
On the existence of sequent calculi
Proof systems are often used to prove that a logic has certain properties, such as decidability or interpolation. Depending on the property, one proof system can be more useful than another in this respect. Sequent calculi are popular proof systems for all kinds of applications. Usually the effectiveness of a sequent calculus comes from the good structural properties that it has. This leads to the question which logics do have good sequent calculi and which do not. In this talk a method to prove negative results of this kind, i.e.~results establishing that a logic does not have certain good calculi, is presented. It makes use of a logical property, uniform interpolation, that is a strengthening of interpolation that is rare in some classes of logics. When applied to modal, intermediate, substructural or intuitionistic modal logics, the method implies that those logics without uniform interpolation do not have sequent calculi with certain good structural properties. On the other hand, the method also provides a general technique to prove that certain logics in these classes do have uniform interpolation. As an example it is shown that Lax Logic, a logic with applications in a number of areas, ranging from algebraic logic to hardware verification, has uniform interpolation.
Rosalie Iemhoff is a professor at Utrecht University, the Netherlands, specializing in mathematical and philosophical logic, with a special interest in proof theory, its aims and its methods. Rosalie studied mathematics at the University of Amsterdam, and obtained a PhD in mathematical logic at the same university in 2001. After spending several years as a postdoc, at the University of California, San Diego, and the Technical University Vienna, she joined the Department of Philosophy at Utrecht University in 2006. In 2018 she received a large grant for a five year research project Optimal Proofs on the proof theory of logics. Rosalie is one of the editor’s in chief of the Journal of Philosophical Logic.
Wednesday 14:00 - 15:00
Between Deterministic and Nondeterministic Quantitative Automata
There is a challenging trade-off between deterministic and nondeterministic automata, where the former suit various applications better, however at the cost of being exponentially larger or even less expressive. This gave birth to many notions in between determinism and nondeterminism, aiming at enjoying, sometimes, the best of both worlds. We analyze the possible generalization of such notions from Boolean to quantitative automata, and suggest that it depends on the following key characteristics of the considered notion---whether it is syntactic or semantic, and if semantic, whether it is word-based or language-based. We classify numerous notions known in the Boolean setting according to their characterization above, generalize them to the quantitative setting and look into relations between them. The generalized notions open new research directions with respect to quantitative automata, and provide insights on the original notions with respect to Boolean automata.
Udi Boker is Professor of Computer Science at the Interdisciplinary Center (IDC) Herzliya, Israel. He specializes in logic, formal verification, computational models, game theory, and automata theory. He received his PhD in computer science from the Tel-Aviv University, and did postdoctoral research in the Hebrew University and in the Institute of Science and Technology (IST) Austria. Prior to joining the academy, he served as an R&D Director in the Hi-Tech company Mercury Interactive, initiating and leading the area of load-testing over the Internet.
Thursday: 14:00 - 15:00
Classification in computable structure theory
In computable structure theory, one studies the computational content of particular encodings of structures. Given a family of structures (such as finite branching trees or free groups), it is natural to want to classify those in the family that are computable. Here we provide a self-contained overview of approaches to classification in this field and explore results about families of structures such as those above.
Karen Lange is an associate professor of mathematics at Wellesley College. Her research is in computability theory; she studies the ''balance scales'' used to calibrate computational information and applies these tools to measure the difficulty of algebraic problems. She earned her undergraduate degree at Swarthmore College and her doctoral degree at the University of Chicago, and she completed an NSF Postdoctoral Fellowship at the University of Notre Dame.
Friday: 10:00 - 11:00
How to develop an intuition for risk. . . and other invisible phenomena
The study of quantitative risk in security systems is often based around complex and subtle mathematical ideas involving probabilities. The notations for these ideas can pose a communication barrier between collaborating researchers even when those researchers are working within a similar framework. In this talk I will describe the use of geometrical representation and reasoning as a way to share ideas using the minimum of (formal) notation so as to build intuition about what kinds of properties might or might not be true. I will describe a faithful geometrical setting for the channel model of quantitative information flow (QIF) and demonstrate how it can facilitate “proofs without words” for problems in the QIF setting.
Annabelle McIver is a professor of Computer Science at Macquarie University in Sydney. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book ''Abstraction, Refinement and Proof for Probabilistic Systems'', and ''The Science of Quantitative Information Flow''.
Saturday: 11:30 - 12:30
Seemingly impossible programs and proofs
In previous work we developed algorithms that perform the seemingly impossible task of exhaustively searching infinite sets in finite time. To formulate and prove their correctness, we used a combination of programming language semantics, topology and higher-type computability theory. In this talk, we explore the same ideas from a different, logical angle. The algorithms are derived from constructive proofs of instances of the law of the excluded middle that, at first sight, look constructively implausible. To achieve this, we work in dependent type theory, a foundation for constructive mathematics that can also be considered as a programming language. Familiarity with type theory will not be assumed.
Martín Escardó is a Professor of Theoretical Computer Science at the School of Computer Science of the University of Birmingham, UK. His research interests include topology, locale theory, domain theory, game theory, homotopy type theory, formalization of mathematics, constructive mathematics. He studied at UFRGS, Brazil, and received a PhD from Imperial College, London. Before joining Birmingham, he was a lecturer at the universities of Edinburgh and St Andrews in Scotland.
|July 5, 2021 (AoE)||-||Abstract submission|
|July 12, 2021 (AoE)||-||Paper Submission|
|September 30, 2021||-||Notification|
|October 29, 2021||-||Final Version Deadline|
|January 31, 2022||-||Registration Speaker|
|February 6, 2022||-||Registration Participants|
|February 14-19, 2022||-||Conference [Online]|
Submitted papers must be in English and must provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a clearly marked technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the PC.
The papers should be submitted via easychair here.
The CSL 2022 conference proceedings will be published in Leibniz International Proceedings in Informatics (LIPIcs), see here.
Authors are invited to submit contributed papers of no more than 15 pages in LIPIcs style (not including references), presenting unpublished work fitting the scope of the conference. Papers may not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or a journal.
Papers authored or co-authored by members of the PC are not allowed.
At least one of the authors of each accepted paper is expected to register for the conference and attend it in person or online, in order to present their papers.
The Helena Rasiowa Award is the best student paper award for the CSL conference series, starting from CSL 2022. The award will be given to the best paper (as decided by the PC) written solely by students or for which students were the main contributors. A student in this context is any person who is currently studying for a degree or whose PhD award date is less than one year prior to the first day of the conference. Read more about the contribution of Helena Rasiowa to logic and computer science, and their interplay, here.
The programme committee selected Antonio Casares as the recipient of the 2022 Helena Rasiowa Award, for his paper On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions.
List of topics
constructive mathematics and type theory
equational logic and term rewriting
automata and games, game semantics
modal and temporal logic
logical aspects of computational complexity
finite model theory
computational proof theory
logic programming and constraints
lambda calculus and combinatory logic
categorical logic and topological semantics
specification, extraction and transformation of programs
logical aspects of quantum computing
logical foundations of programming paradigms
verification and program analysis
Benedikt Bollig (Cachan, France)
Agata Ciabattoni (Vienna, Austria)
Liron Cohen (Ben-Gurion University, Israel)
Anupam Das (Birmingham, UK)
Claudia Faggian (Paris, France)
Francesco Gavazzo (Bologna, Italy)
Stefan Göller (Kassel, Germany)
Willem Heijltjes (Bath, UK)
Sandra Kiefer (Aachen, Germany)
Emanuel Kieronski (Wroclaw, Poland)
Bartek Klin (Warsaw, Poland)
Juha Kontinen (Helsinki, Finland)
Anthony Lin (Kaiserslautern, Germany)
Karoliina Lehtinen (Marseille, France)
Florin Manea (Göttingen, Germany, co-chair)
Fredrik Nordvall Forsberg (Strathclyde, UK)
Liat Peterfreund (Paris, France and Edinburgh, UK)
Daniela Petrisan (Paris, France)
Karin Quaas (Lepizig)
Alex Simpson (Ljubljana, Slovenia, co-chair)
Pawel Sobocinski (Tallin, Estonia)
Ana Sokolova (Salzburg, Austria)
Linda Brown Westrick (Connecticut, US)
Fundamentals of Computer Science Group at University of Göttingen, Germany. Maria Kosche, Tore Koß, Florin Manea (chair), Patricia Nitzke, Viktoriya Pak, Stefan Siemer.
Please send all questions about submissions to the PC co-chairs: firstname.lastname@example.org
Monday 14.02.2022The Logic Mentoring Workshop @ CSL.
Sunday 20.02.2022The Twenty Second International Workshop on Logic and Computational Complexity LCC 2022.
All times are UTC+1, i.e., the timezone of Göttingen, Germany.
General instructions and information for the speakers can be found here.
|Tuesday: 09:50 - 10:00||Opening||-|
|Tuesday: 10:00 - 11:00||On the existence of sequent calculi Utrecht University, The Netherlands||Invited Talk: Rosalie Iemhoff. Session Chair: Bartek Klin|
|Tuesday: 11:00 - 11:30||Break||-|
|Tuesday: 11:30 - 12:30||Session Chair: Dietrich Kuske||-|
|Tuesday: 11:30 - 11:55||Weighted Automata and Expressions over Pre-Rational Monoids||Nicolas Baudru, Louis-Marie Dando, Nathan Lhote, Benjamin Monmege, Pierre-Alain Reynier and Jean-Marc Talbot.|
|Tuesday: 11:55 - 12:20||Revisiting Synthesis for One-Counter Automata||Ritam Raha and Guillermo Pérez.|
|Tuesday: 12:20 - 14:00||Lunch||-|
|Tuesday: 14:00 - 15:15||Session Chair: Mariangiola Dezani||-|
|Tuesday: 14:00 - 14:25||Encoding Tight Typing in a Unified Framework||Delia Kesner and Andrés Ezequiel Viso.|
|Tuesday: 14:25 - 14:50||Useful Open Call-by-Need||Beniamino Accattoli and Maico Leberle.|
|Tuesday: 14:50 - 15:15||Games, mobile processes, and functions||Guilhem Jaber and Davide Sangiorgi.|
|Tuesday: 15:15 - 15:45||Break||-|
|Tuesday: 15:45 - 17:00||Session Chair: Michael Benedikt||-|
|Tuesday: 15.45 - 16:10||Succinct Graph Representations of mu-Calculus Formulas||Clemens Kupke, Johannes Marti and Yde Venema.|
|Tuesday: 16:10 - 16:35||Number of Variables for Graph Identification and the Resolution of GI Formulas||Jacobo Torán and Florian Wörz.|
|Tuesday: 16:35 - 17:00||MSO undecidability for some hereditary classes of unbounded clique-width||Anuj Dawar and Abhisekh Sankaran.|
|Tuesday: 17:00 - open||Get-together||-|
|Wednesday: 10:00 - 11:15||Session Chair: Anupam Das||-|
|Wednesday: 10:00 - 10:25||Cyclic proofs for transfinite expressions||Emile Hazard and Denis Kuperberg.|
|Wednesday: 10:25 - 10:50||BV and Pomset Logic are not the same||Lê Thành Dũng Nguyễn and Lutz Straßburger.|
|Wednesday: 10:50 - 11:15||Parallelism in Soft Linear Logic||Paulin Jacobé De Naurois.|
|Wednesday: 11:15 - 11:45||Break||-|
|Wednesday: 11:45 - 12:35||Session Chair: Sandra Kiefer||-|
|Wednesday: 11:45 - 12:10||Differential games, locality, and model checking for FO logic of graphs||Jakub Gajarský, Stephan Kreutzer and Maximilian Gorsky.|
|Wednesday: 12:10 - 12:35||On the complexity of SPEs in parity games||Léonard Brice, Jean-Francois Raskin and Marie Van Den Bogaard.|
|Wednesday: 12:35 - 14:00||Lunch||-|
|Wednesday 14:00 - 15:00||Between Deterministic and Nondeterministic Quantitative Automata IDC Herzliya, Israel||Invited Talk: Udi Boker. Session Chair: Florin Manea|
|Wednesday: 15:00 - 15:30||Break||-|
|Wednesday: 15:30 - 16:45||Session Chair: Udi Boker||-|
|Wednesday: 15:30 - 15:55||Decidability for Sturmian words||Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz and Jeffrey Shallit.|
|Wednesday: 15:55 - 16:20||Inferring Symbolic Automata||Dana Fisman, Hadar Frenkel and Sandra Zilles.|
|Wednesday: 16:20 - 16:45||Spatial Existential Positive Logics for Hyperedge Replacement Grammars||Yoshiki Nakamura.|
|Wednesday: 16:45 - 17:15||Break||-|
|Wednesday: 17:15 - 18:05||Session Chair: Sandra Kiefer||-|
|Wednesday: 17:15 - 17:40||First-Order Logic with Connectivity Operators||Nicole Schirrmacher, Sebastian Siebertz and Alexandre Vigny.|
|Wednesday: 17:40 - 18:05||Structural properties of the first-order transduction quasiorder||Jaroslav Nesetril, Patrice Ossona de Mendez and Sebastian Siebertz.|
|Wednesday: 18:10 - open||Annual membership meeting of EACSL||Every participant to CSL is encouraged to attend this meeting.|
|Thursday: 10:00 - 11:15||Session Chair: Martín Escardó||-|
|Thursday: 10:00 - 10:25||Synthetic Integral Cohomology in Cubical Agda||Guillaume Brunerie, Axel Ljungström and Anders Mörtberg.|
|Thursday: 10:25 - 10:50||Gardening with the Pythia||Martin Baillon, Assia Mahboubi and Pierre-Marie Pédrot.|
|Thursday: 10:50 - 11:15||Generalized Universe Hierarchies and First-Class Universe Levels||András Kovács.|
|Thursday: 11:15 - 11:45||Break||-|
|Thursday: 11:45 - 12:35||Session Chair: Anupam Das||-|
|Thursday: 11:45 - 12:10||Realising Intensional S4 and GL Modalities||Liang-Ting Chen and Hsiang-Shang Ko.|
|Thursday: 12:10 - 12:35||Planar realizability via left and right applications||Haruka Tomita.|
|Thursday: 12:35 - 14:00||Lunch||-|
|Thursday: 14:00 - 15:00||Classification in computable structure theory Wellesley College, USA||Invited Talk: Karen Lange. Session Chair: Rosalie Iemhoff|
|Thursday: 15:00 - 15:30||Break||-|
|Thursday: 15:30 - open||Awards||-|
|Thursday: 15:30 - 16:00||Helena Rasiowa Award||-|
|Thursday: 16:05 - 17:00||Ackermann Award: Marie Fortin||-|
|Thursday: 17:05 - 18:00||Ackermann Award: Sandra Kiefer||-|
|Friday: 10:00 - 11:00||How to develop an intuition for risk. . . and other invisible phenomena University Sydney, Australia||Invited Talk: Annabelle McIver. Session Chair: Maribel Fernandez|
|Friday: 11:00 - 11:30||Break||-|
|Friday: 11:30 - 12:20||Session Chair: Martin Ziegler||-|
|Friday: 11:30 - 11:55||(cancelled) Constructing the space of valuations of a quasi-Polish space as a space of ideals||Matthew de Brecht.|
|Friday: 11:55 - 12:20||Dynamic Cantor Derivative Logic||David Fernández-Duque and Yoàv Montacute.|
|Friday: 12:20 - 14:00||Lunch||-|
|Friday: 14:00 - 15:15||Session Chair: Ana Sokolova||-|
|Friday: 14:00 - 14:25||Localisable monads||Carmen Maria Constantin, Nuiok Dicaire and Chris Heunen.|
|Friday: 14:25 - 14:50||An Internal Language for Categories Enriched over Generalised Metric Spaces||Fredrik Dahlqvist and Renato Neves.|
|Friday: 14:50 - 15:15||Fuzzy algebraic theories||Davide Castelnovo and Marino Miculan.|
|Friday: 15:15 - 15:45||Break||-|
|Friday: 15:45 - 17:00||Session Chair: Damian Niwinski||-|
|Friday: 15:45 - 16:10||Optimal strategies in concurrent reachability games||Benjamin Bordais, Patricia Bouyer and Stephane Le Roux.|
|Friday: 16:10 - 16:35||Finite-memory winning strategies in Δ⁰₂||Patricia Bouyer, Stephane Le Roux and Nathan Thomasset.|
|Friday: 16:35 - 17:00||Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory||Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Ruediger Olderog.|
|Friday: 17:00 - 17:30||Break||-|
|Friday: 17:30 - 18:20||Session Chair: Jean Goubault-Larrecq||-|
|Friday: 17:30 - 17:55||Constructive Many-one Reduction from the Halting Problem to Semi-unification||Andrej Dudenhefner.|
|Friday: 17:55 - 18:20||Anti-unification of Unordered Goals||Gonzague Yernaux and Wim Vanhoof.|
|Friday: 18:20 - open||Get-together||-|
|Saturday: 10:00 - 10:50||Session Chair: Florin Manea||-|
|Saturday: 10:00 - 10:25||Simulation by Rounds of Letter-to-Letter Transducers||Antonio Abu Nassar and Shaull Almagor.|
|Saturday: 10:25 - 10:50||On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions||Antonio Casares.|
|Saturday: 10:50 - 11:30||Break||-|
|Saturday: 11:30 - 12:30||Seemingly impossible programs and proofs University of Birmingham, UK||Invited Talk: Martin Escardo. Session Chair: Alex Simpson|
|Saturday: 12:30 - 12:40||Closing||-|