ICALP INVITED SPEAKERS
Anuj Dawar
University of Cambridge
Danupon Nanongkai
MPI Saarbrücken
Merav Parter
Weizmann Institute
FSCD INVITED SPEAKERS
Delia Kesner
Université Paris Cité
Bettina Könighofer
TU Graz
Sebastian Ullrich
LEAN-FRO
ICALP 2024
51st EATCS International Colloquium on Automata, Languages and Programming
ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). ICALP 2024 will be preceded by a series of workshops, which will take place on July 7, 2024.
ICALP 2024 is organized by the Department of Software Science, Tallinn University of Technology, in cooperation with the European Association for Theoretical Computer Science (EATCS).
The first ICALP conference was organized in 1972. For more information about previous editions, see the EATCS webpage http://eatcs.org/index.php/international-colloquium.
Important dates
- Submissions: February 14, 2024 at 1pm CET
- Rebuttal: March 26-29, 2024
- Author notification: April 14, 2024
- Camera-ready version: April 28, 2024
- Early registration: May 17, 2024
- Conference: July 8-12, 2024
- ICALP Workshops: July 6-7, 2024
Submissions
Paper submissions are handled via Easychair.
1) Papers must present original research on the theory of computer science. No prior publication and no simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Authors are encouraged to also make full versions of their submissions freely accessible in an on-line repository such as ArXiv, HAL, ECCC.
2) Submissions take the form of an extended abstract of no more than 15 pages, excluding references and a clearly labelled appendix. The appendix may consist either of omitted proofs or of a full version of the submission, and it will be read at the discretion of program committee members. The use of the LIPIcs document class is an option, but not required. The extended abstract has to present the merits of the paper and its main contributions clearly, and describe the key concepts and technical ideas used to obtain the results. Submissions must provide the proofs which can enable the main mathematical claims of the paper to be verified.
3) Submissions are anonymous. The conference will employ a lightweight double-blind reviewing process. Submissions should not reveal the identity of the authors in any way. Authors should ensure that any references to their own related work are in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).
The purpose of this double-blind process is to help PC members and external reviewers come to an initial judgment about the paper without bias, and not to make it impossible for them to discover who the authors are if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult. In particular, important references should not be omitted. In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For example, authors may post drafts of their papers on the web, submit them to arXiv, and give talks on their research ideas.
4) Submissions authored or co-authored by members of the program committee are allowed.
5) The submissions are done via Easychair to the appropriate track of the conference (see topics below). The use of pdflatex or similar pdf generating tools is mandatory and the page limit is strict (see point 2.) Papers that deviate significantly from these requirements risk rejection without consideration of merit.
6) During the rebuttal phase, authors will have from March 26-29, 2024 to view and respond to initial reviews. Further instructions will be sent to authors of submitted papers before that time.
7) At least one author of each accepted paper is expected to register for the conference, and all talks are in-person. In exceptional cases, there may be support for remotely presenting a talk.
8) Papers authored only by students should be marked as such upon submission in order to be eligible for the best student paper awards of the track.
SafeToC
ICALP has joined http://safetoc.org.
Participants have to follow the ICALP code of conduct.
The ICALP 2024 SafeToc advocate is Diana Kessler.
ICALP TRACKS
Papers presenting original research on all aspects of theoretical computer science are sought. Typical, but not exclusive, topics of interest are:
Track A
`Algorithms, Complexity and Games
- Algorithmic and Complexity Aspects of Network Economics
- Algorithmic Aspects of Biological and Physical Systems
- Algorithmic Aspects of Networks and Networking
- Algorithmic Aspects of Security and Privacy
- Algorithmic Game Theory and Mechanism Design
- Approximation and Online Algorithms
- Combinatorial Optimization
- Combinatorics in Computer Science
- Computational Complexity
- Computational Geometry
- Computational Learning Theory
- Cryptography
- Data Structures
- Design and Analysis of Algorithms
- Distributed and Mobile Computing
- Foundations of Machine Learning
- Graph Mining and Network Analysis
- Parallel and External Memory Computing
- Parameterized Complexity
- Quantum Computing
- Randomness in Computation
- Sublinear Time and Streaming Algorithms
- Theoretical Foundations of Algorithmic Fairness
Track B
Automata, Logic, Semantics, and Theory of Programming
- Algebraic and Categorical Models of Computation
- Automata, Logic, and Games
- Database Theory, Constraint Satisfaction Problems, and Finite Model Theory
- Formal and Logical Aspects of Learning
- Formal and Logical Aspects of Security and Privacy
- Logic in Computer Science and Theorem Proving
- Models of Computation: Complexity and Computability
- Models of Concurrent, Distributed, and Mobile Systems
- Models of Reactive, Hybrid, and Stochastic Systems
- Principles and Semantics of Programming Languages
- Program Analysis, Verification, and Synthesis
- Type Systems and Typed Calculi
Accepted papers
Track A
Kernelization Dichotomies for Hitting Subgraphs under Structural ParameterizationsA Faster Algorithm for Pigeonhole Equal SumsRefuting approaches to the log-rank conjecture for XOR functionsOn the Smoothed Complexity of Combinatorial Local SearchLower Bounds on 0-Extension with Steiner NodesTowards Tight Bounds for the Graph Homomorphism Problem Parameterized by Cutwidth via Asymptotic Matrix ParametersTwo-sets cut-uncut on planar graphsStreaming Edge Coloring with Subquadratic Palette SizePath-Reporting Distance Oracles with Logarithmic Stretch and Linear SizeLinear Relaxed Locally Decodable and Correctable Codes Do Not Need Adaptivity and Two-Sided ErrorLipschitz Continuous Allocations for Optimization GamesBayesian Calibrated Click-Through AuctionsSubexponential Parameterized Directed Steiner Network Problems on Planar Graphs: a Complete ClassificationSubquadratic Submodular Maximization with a General Matroid ConstraintBQP, meet NP: Search-to-decision reductions and approximate countingTowards an Analysis of Quadratic ProbingAlphabet Reduction for Reconfiguration ProblemsTwo Choices are Enough for P-LCPs, USOs, and Colorful TangentsParameterized Algorithms for Steiner Forest in Bounded Width GraphsThe k-Opt algorithm for the Traveling Salesman Problem has exponential running time for k > 5Vital Edges for (s,t)-mincut: Efficient Algorithms, Compact Structures, & Optimal Sensitivity OraclesSolution discovery via reconfiguration for problems in PAlmost-Tight Bounds on Preserving Cuts in Classes of Submodular HypergraphsCaching Connections in MatchingsStreaming Algorithms for Connectivity AugmentationOn the cut-query complexity of approximating max-cutNo Polynomial Kernels for KnapsackÕptimal Dynamic Time Warping on Run-Length Encoded StringsOptimal PSPACE-hardness of Approximating Set Cover ReconfigurationFaster Algorithms for Dual-Failure Replacement PathsAlgorithms for the Generalized Poset Sorting ProblemThe Group Access Bounds for Binary Search TreesRobot positioning using torus packing for multisetsDelineating Half-Integrality of the Erdős-Pósa Property for Minors: the Case of SurfacesA Sublinear Time Tester for Max-Cut on Clusterable GraphsCut Sparsification and Succinct Representation of Submodular HypergraphsSolving Woeginger’s Hiking Problem: Wonderful Partitions in Anonymous Hedonic GamesVertex-minor universal graphs for generating entangled quantum subsystemsTesting Spreading Behavior in Networks with Arbitrary TopologiesA Characterization of Complexity in Public Goods GamesSplitting-off in HypergraphsOracle-Augmented Prophet InequalitiesDynamic PageRank: Algorithms and Lower BoundsThe Bit Complexity of Dynamic Algebraic Formulas and their DeterminantsApproximation Algorithms for lp-Shortest Path and lp-Group Steiner TreeFully Dynamic Strongly Connected Components in Planar DigraphsDetecting Disjoint Shortest Paths in Linear Time and MoreLimits of Sequential Local Algorithms on the Random k-XORSAT ProblemApproximate counting for spin systems in sub-quadratic timeRandom Separating Hyperplane Theorem and Learning PolytopesNew Tradeoffs for Decremental Approximate All-Pairs Shortest PathsA Multivariate to Bivariate Reduction for Noncommutative Rank and Related ResultsImproved Lower Bounds for Approximating Parameterized Nearest Codeword and Related Problems under ETHFully-Scalable MPC Algorithms for Clustering in High DimensionComputing Tree Decompositions with Small Independence NumberAnother Hamiltonian cycle in bipartite Pfaffian graphsExploiting Automorphisms of Temporal Graphs for Fast Exploration and RendezvousList Update with Delays or Time WindowsConstrained Level Planarity is FPT with Respect to the Vertex Cover NumberAn FPRAS for two terminal reliability in directed acyclic graphsIsomorphism for Tournaments of Small Twin WidthOptimal Non-Adaptive Cell Probe Dictionaries and HashingA Tight Subexponential Algorithm for Two-Page Book EmbeddingFundamental Problems on Bounded-Treewidth Graphs: The Real Source of HardnessFast Approximate Counting of CyclesBreaking a Barrier in Constructing Compact Indexes for Parameterized Pattern MatchingOptimal Electrical Oblivious Routing on ExpandersPolylogarithmic Approximations for Robust s-t PathAdaptive sparsification for matroid intersectionBetter Sparsifiers for Directed Eulerian GraphsA Note on Approximating Weighted Nash Social Welfare with Additive ValuationsAn improved integrality gap for disjoint cycles in planar graphsTesting Ck-freeness in bounded-arboricity graphsExponential lower bounds via exponential sumsOn the Space Usage of Approximate Distance Oracles with Sub-2 StretchFiner-grained Reductions in Fine-grained Hardness of ApproximationLower Bounds for Matroid Optimization Problems with a Linear ConstraintOne-Way Communication Complexity of Partial XOR FunctionsAn O(loglog n)-Approximation for Submodular Facility LocationSharp Noisy Binary Search with Monotonic ProbabilitiesDecremental Matching in General Weighted GraphsBetter space-time-robustness trade-offs for set reconciliationSimultaneously Approximating All lp-norms in Correlation ClusteringSublinear Algorithms for TSP via Path CoversNearly optimal independence oracle algorithms for edge estimation in hypergraphsFrom Trees to Polynomials and Back Again: New Capacity Bounds with Applications to TSPOracle separation of QMA and QCMA with bounded adaptivityLow-Memory Algorithms for Online Edge ColoringParameterized Algorithms for Coordinated Motion Planning: Minimizing EnergyAn Optimal Sparsification Lemma for Low-Crossing Matchings and its ApplicationsTight Bounds on Adjacency Labels for Monotone Graph ClassesParallel and Sequential Hardness of Hierarchical Graph ClusteringAn improved Quantum Max Cut approximation via Maximum MatchingProblems in NP can Admit Double-Exponential Lower Bounds when Parameterized by Treewidth and Vertex CoverStreaming Edge Coloring with Asymptotically Optimal ColorsDistributed fast crash-tolerant consensus with nearly-linear quantum communicationThe Discrepancy of Shortest PathsA spectral approach to approximately counting independent sets in dense bipartite graphsTwo-Source and Affine Non-Malleable Extractors for Small EntropyNP-hardness of testing equivalence to sparse polynomials and constant support polynomialsBetter Decremental and Fully Dynamic Sensitivity Oracles for Subgraph ConnectivityFrom Proof Complexity to Circuit Complexity via Interactive ProtocolsFinding Most Shattering Minimum Vertex Cuts of Polylogarithmic Size in Near-Linear TimeHigh-Accuracy Multicommodity Flows via Iterative RefinementAdditive Spanner Lower Bounds with Optimal Inner Graph StructureImpagliazzo's Worlds Through the Lens of Conditional Kolmogorov ComplexityOptimal Bounds for Distinct QuarticsNon-Linear PagingA tight Monte-Carlo algorithm for Steiner Tree parameterized by clique-widthMinimizing Symmetric Convex Functions over Hybrid of Continuous and Discrete Convex SetsApproximation Schemes for Geometric Knapsack for Packing Spheres and Fat ObjectsLearning low-degree quantum objectsMinimizing Tardy Processing Time on a Single Machine in Near-Linear TimeProblems on Group-labeled Matroid BasesParameterized Approximation for Robust Clustering in Discrete Geometric SpacesQuantum Algorithms for Graph Coloring and other Partitioning, Covering, and Packing ProblemsOn the Streaming Complexity of Expander DecompositionSatisfiability to Coverage in Presence of Fairness, Matroid, and Global ConstraintsBounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle
Track B
On the Length of Strongly Monotone Descending Chains over ℕᵈSolving promise equations over monoids and groupsAutomata-Theoretic Characterisations of Branching-Time Temporal LogicsThe Threshold Problem for Hypergeometric Sequences with Quadratic ParametersFinite-memory Strategies for Almost-sure Energy-MeanPayoff Objectives in MDPsFO logic on cellular automata orbits equals MSO logicImproved Algorithm for Reachability in d-VASSFunctional Closure Properties of Finite N-weighted AutomataDomain Reasoning In TopKATFlattability of Priority Vector Addition SystemsIdentifying Tractable Quantified Temporal Constraints within Ord-HornInteger Linear-Exponential Programming in NP by Quantifier EliminationAn order out of nowhere: a new algorithm for infinite-domain CSPsOn Homomorphism Indistinguishability and Hypertree DepthThe complexity of computing in continuous time: space complexity is precisionSmoothed analysis of deterministic discounted and mean-payoff gamesA Complete Quantitative Axiomatisation of Behavioural Distance of Regular ExpressionsDecidability of Graph Neural Networks via Logical CharacterizationsThe structure of trees in the pushdown hierarchyLookahead Games and Efficient Determinisation of History-Deterministic Büchi AutomataOn Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy WordsHomogeneity and Homogenizability: Hard Problems for the Logic SNPA finite presentation of treewidth at most 3 graphsForcing, Transition Algebras, and CalculiOn classes of bounded tree rank, their interpretations, and efficient sparsificationRegular Expressions with Backreferences and Lookaheads Capture NLOGDeciding Linear Height and Linear Size-to-Height Increase of Macro Tree TransducersEdit Distance of Finite State TransducersAn efficient quantifier elimination procedure for Presburger arithmeticT-Rex: Termination of Recursive Functions using Lexicographic Linear CombinationsVerification of Population Protocols with Unordered DataThe 2-Dimensional Constraint Loop Problem is DecidableSeparability in Büchi Vass and Singly Non-Linear Systems of InequalitiesFunction spaces for orbit-finite sets
ICALP COMMITTEES
Conference chair
Pawel Sobocinski (Tallinn University of Technology)
Organising committee
- Niccolò Veltri (Tallinn University of Technology)
- Amar Hadzihasanovic (Tallinn University of Technology)
- Fosco Loregian (Tallinn University of Technology)
- Matt Earnshaw (Tallinn University of Technology)
- Diana Kessler (Tallinn University of Technology)
- Ekaterina Zhuchko (Tallinn University of Technology)
- Juhan Ernits (Tallinn University of Technology)
- Kristi Ainen (Tallinn University of Technology)
- Arianna Jater (Tallinn University of Technology)
- Mariann Lugus (Tallinn University of Technology)
Proceedings chair
Gabriele Puppis (University of Udine, Italy)
Workshop chairs
- Valentin Blot (ENS Paris-Saclay)
- Valia Mitsou (IRIF, University Paris Cité)
- Ekaterina Zhuchko (Tallinn University of Technology)
Programme Commitee (Track A)
Chairs: Karl Bringmann (Saarland University, Germany) and Ola Svensson (EPFL, Switzerland)
- Nima Anari (Stanford University)
- Karl Bringmann (co-chair, Saarland University)
- Parinya Chalermsook (Aalto University)
- Vincent Cohen-Addad (Google Research)
- Jose Correa (Universidad de Chile)
- Holger Dell (Goethe University Frankfurt)
- Ilias Diakonikolas (University of Wisconsin-Madison)
- Yuval Filmus (Technion)
- Arnold Filtser (Bar Ilan University)
- Naveen Garg (IIT Delhi)
- Pawel Gawrychowski (University of Wrocław)
- Anupam Gupta (Carnegie Mellon University)
- Samuel Hopkins (MIT)
- Sophie Huiberts (Columbia University)
- Giuseppe Italiano (LUISS University)
- Michael Kapralov (EPFL)
- Eun Jung Kim (Université Paris-Dauphine)
- Sándor Kisfaludi-Bak (Aalto University)
- Tomasz Kociumaka (Max-Planck-Institute for Informatics)
- Fabian Kuhn (University of Freiburg)
- Amit Kumar (IIT Delhi)
- William Kuszmaul (Harvard University)
- Rasmus Kyng (ETH Zurich)
- Kasper Green Larsen (Aarhus University)
- François Le Gall (Nagoya University)
- Pasin Manurangsi (Google Research)
- Daniel Marx (CISPA Helmholtz Center for Information Security)
- Yannic Maus (TU Graz)
- Nicole Megow (University of Bremen)
- Ruta Mehta (University of Illinois at Urbana-Champaign)
- Jakob Nordström (University of Copenhagen)
- Richard Peng (University of Waterloo)
- Seth Pettie (University of Michigan)
- Adam Polak (Bocconi University)
- Lars Rohwedder (Maastricht University)
- Eva Rotenberg (DTU Compute)
- Sushant Sachdeva (University of Toronto)
- Melanie Schmidt (University of Cologne)
- Sebastian Siebertz (University of Bremen)
- Shay Solomon (Tel Aviv University)
- Nick Spooner (University of Warwick)
- Clifford Stein (Columbia University)
- Ola Svensson (co-chair, EPFL)
- Luca Trevisan (Bocconi University)
- Ali Vakilian (Toyota Technological Institute Chicago)
- Jan van den Brand (Georgia Tech)
- Erik Jan van Leeuwen (Utrecht University)
- Oren Weimann (University of Haifa)
- Nicole Wein (University of Michigan)
- Andreas Wiese (TU Munich)
- John Wright (UC Berkeley)
Programme Committee (Track B)
Chair: Martin Grohe (RWTH Aachen University)
- Arnold Beckmann (Swansea University)
- Manuel Bodirsky (TU Dresden)
- Patricia Bouyer (CNRS, LMF)
- Yijia Chen (Shanghai Jiao Tong University)
- Victor Dalmau (Universitat Pompeu Fabra)
- Laurent Doyen (CNRS, LMF)
- Marcelo Fiore (Cambridge University)
- Stefan Göller (University of Kassel)
- Martin Grohe (RWTH Aachen University, chair)
- Sandra Kiefer (Oxford University)
- Aleks Kissinger (Oxford University)
- Bartek Klin (Oxford University)
- Antonin Kucera (Masaryk University Brno)
- Carsten Lutz (University of Leipzig)
- Jerzy Marcinkowski (University of Wrocław)
- Annabelle McIver (Macquaire University Sydney)
- Andrzej Murawski (Oxford University)
- Paweł Parys (University of Warsaw)
- Michał Pilipczuk (University of Warsaw)
- Joel Ouaknine (Max Planck Institute for Software Systems)
- Christian Riveros (Pontificia Universidad Catolica de Chile)
- Alexandra Silva (Cornell University)
- Balder ten Cate (ILLC Amsterdam)
- Szymon Toruńczyk (University of Warsaw)
- Igor Walukiewicz (CNRS, University of Bordeaux)
- Sarah Winter (IRIF, University Paris Cité)
- Georg Zetzsche (Max Planck Institute for Software Systems)
- Martin Ziegler (KAIST)
Registration
All prices are in euros and include 22% VAT. Note that every accepted paper requires at least one regular (non-student) registration.
The prices listed below are the early bird prices, valid until May 17.
| Early bird | All inclusive | ICALP 2024 | LiCS 2024 | FSCD 2024 | Workshops (1 day) | Workshops (2 days) | Workshops (3 days) | Workshops (unlimited) |
|---|---|---|---|---|---|---|---|---|
| Regular non-member | 1000 | 800 | 640 | 640 | 80 | 160 | 240 | 320 |
| Regular member | 950 | 750 | 590 | 590 | ||||
| Student non-member | 780 | 600 | 480 | 480 | 60 | 120 | 180 | 240 |
| Student member | 730 | 550 | 430 | 430 |
The prices listed below are the late registration prices, in place after May 17.
| Late registration | All inclusive | ICALP 2024 | LiCS 2024 | FSCD 2024 | Workshops (1 day) | Workshops (2 days) | Workshops (3 days) | Workshops (unlimited) |
|---|---|---|---|---|---|---|---|---|
| Regular non-member | 1200 | 960 | 770 | 770 | 100 | 200 | 300 | 400 |
| Regular member | 1150 | 910 | 720 | 720 | ||||
| Student non-member | 780 | 720 | 580 | 580 | 80 | 160 | 240 | 320 |
| Student member | 730 | 670 | 530 | 530 |
Membership discounts
The relevant membership disounts apply as follows: for ICALP an EATCS membership, for LiCS an ACM/ACM SigLog/IEEE membership, for FSCD an ACM/ACM SigLog/ACM SIGPLAN membership. Any of the above memberships qualifies for a discounted all-inclusive price.
Workshop participation
Conference participants who purchase a conference-specific registration (i.e. ICALP, LiCS or FSCD) and who also wish to attend workshops need to purchase an additional workshop registration, depending on how many days of workshops they wish to attend.
An exception to this rule is when a participant has registered to a conference and would like to attend a workshop on the same day that the conference is scheduled -- in this case no additional fee is necessary for that day, but we ask that you email [email protected] with the details of your registration and the additional workshop(s) you would like to attend so that we can keep an accurate track of the numbers of participants.
The all-inclusive price includes access to all three conferences and unlimited workshop participation.
Welcome reception, Tuesday 9 July
All conference registrations include a ticket to the Welcome reception at Kadriorg Art Museum, Weizengergi 37, on the evening of Tuesday 9 July.
Joint banquet, Wednesday 10 July
The joint banquet will be held on Wednesday 10 July at the Tallinn Seaplane Harbour Museum. All participants who want to attend the banquet must purchase a banquet ticket separately -- the early bird price until May 17 is 85 euros per banquet ticket, the price after May 17 is 100 euros. Additional banquet tickets can be purchased for accompanying people. Note that the all-inclusive price does not include a banquet ticket.
To register, please click on the following link. Our partner Fienta takes payments and provides invoices. For questions regarding registration please email [email protected].
Cancellations and refunds
Cancellations should be notified in writing by e-mail to [email protected]. Your cancellation will be confirmed in writing.
Cancellations are subject to the following conditions:
- Cancellations received by May 31, 2024: 10% is held as an administrative fee.
- Cancellations received after May 31, 2024: no refund will be made.
All refunds will be processed after the meeting.
Letter of Confirmation of Participation
A Letter of Confirmation of participation for VISA Applications or other purposes can be requested by e-mail to [email protected]. Letters of Confirmation will only be issued for fully registered presenters, e.g. an accepted article + full payment of the registration fees is required. Issuace of the visa will depend on a relevant official. In case the presenter will be denied the visa, a full refund will be made even after May 31. The organizers of the conference will not take any financial responsibilities of the potential costs of a delegate travelling to and during the stay in Estonia. Details on visa and consular issues, crossing the border, etc. are available at the MFA of Estonia.
Programme
The table below shows an overview of the schedule for the three conferences and associated events. Click on a session for more detail. You can also download the conference booklet in pdf, although the programme there is out of date, the up-to-date programme is the online version below.
| Monday 8 July | Tuesday 9 July | Wednesday 10 July | Thursday 11 July | Friday 12 July | Saturday 13 July | ||||||||
| Morning | Silva | Dawar | Weirich | Parter | Elkind | Ullrich | |||||||
| LiCS S1, S2 | ICALP A1, A2 | LiCS S4 | ICALP B1, A6, A7, A8 | LiCS S6 | FSCD S1 | ICALP B3, A12, A13 | LiCS S8 | FSCD S3 | ICALP joint A/B session, A14, A15 | FSCD S5 | ICALP B5, A18, A19, A20 | FSCD S7 | |
| Lunch | LiCS SC | ICALP SC | EATCS council | FSCD SC | |||||||||
| Afternoon | Simpson | Nanongkai | LiCS S5 | ICALP B2, A9, A10, A11 | LiCS S7 | FSCD S2 | ICALP best papers | Escardó | Kesner | FSCD S8 | |||
| LiCS S3 | ICALP A3, A4, A5 | LICS S9 | FSCD S4 | ICALP B4, A16, A17 | FSCD S6 | ICALP B6, A21, A22, A23 | |||||||
| FSCD business | |||||||||||||
| Gödel prize | Buss | Bloem | EATCS award | ||||||||||
| LiCS business | Church award | LiCS posters | |||||||||||
| LiCS ToT | EATCS assembly | ||||||||||||
| Presburger awards | ICALP business meeting | ||||||||||||
| Evening | Welcome reception, Kadriorg Art Museum | Joint banquet, Seaplane Harbour Museum | |||||||||||
The table below shows the timing of the workshops vis a vis the main conferences. Click on a workshop for its programme.
| Saturday 6 July | Sunday 7 July | Monday 8 July | Tuesday 9 July | Wednesday 10 July | Thursday 11 July | Friday 12 July | Saturday 13 July |
| PAAW | AATG | LiCS | |||||
| GETCO D1 D2 | ICALP | ||||||
| TAT | LearnAut | LFMTP | IWC | FSCD | |||
| SmP | TLLA D1 D2 | ||||||
| PACS | MSFP | ITRS | |||||
| LMW | Women in Logic | ||||||
Detailed programme
Saturday July 6 workshops
| TIME | PAAW A346 |
GETCO A121 |
TAT A224 |
| 09:00 | Matthias Kaul. A (1.5+ε)-Approximation for Multiple TSP with a Variable Number of Depots | Opening |
Opening |
| 09:15 | Tutorial: Uli Fahrenberg. Directed algebraic topology and concurrency I | Invited talk. Olivier Bournez. Characterisations of polynomial-time and -space complexity classes using (discrete) ordinary differential equations | |
| 09:30 | George Ospinov. Constant-Factor FPT-Approximation Dichotomies for MinCSPs | ||
| 09:45 | |||
| 10:00 | Coffee break | ||
| 10:30 | Tutorial: Uli Fahrenberg. Directed algebraic topology and concurrency II | Invited tutorial. Alessio Mansutti. Existential Presburger Arithmetic with Divisibility Constraints: A tour | |
| 11:00 | Ilan
Doron-Arad. Budgeted Matroid Maximization: a Parameterized Viewpoint |
||
| 11:15 | |||
| 11:30 | Catarina
Faustino. On the topology of concurrent systems |
||
| 12:00 | Yijia Chen. Simple Combinatorial Construction of the ko(1)-Lower Bound for Approximating the Parameterized k-Clique | Invited talk. Žaneta Semanišinová. Identifying Tractable Quantified Temporal Constraints | |
| 12:30 | |||
| 12:45 | Lunch | ||
| 14:00 | Amit Gadekar. Parameterized Approximation Schemes for Clustering with General Norm Objectives | Tutorial: Jérémy Ledent. The simplicial approach to distributed computing | Invited tutorial. Sławomir Lasota. Orbit-finite linear programming |
| 14:30 | Fateme Abbasi. Parameterized Approximation for Robust Clustering in Discrete Geometric Spaces | ||
| 15:00 | Tanmay Inamdar. FPT approximation for Covering and Clustering with Outliers. | ||
| 15:30 | Coffee break | ||
| 16:00 | Mahdi Cheraghchi. Parameterized Inapproximability of the Minimum Distance Problem over All Fields and the Shortest Vector Problem in All Ip Norms | Ahmed Bouabdallah. The fractal nature of the properties of reactive and concurrent programs. | Invited talk. Joris Nieuwveld. Logical theories combined with multiple powers |
| 16:30 | Yuwei Liu. Improved Lower Bounds for Approximating Parameterized Nearest Codeword and Related Problems under ETH | ||
| 17:00 | Open problem session | Safa Zouari. Bisimulations and Logics for Higher-Dimensional Automata. | |
Sunday July 7 workshops
| TIME | AATG A224 |
GETCO A121 |
LEARNAUT Europe Hall - A222 |
SMP A402 |
PACS A325 |
LMW A346 |
| 09:00 | Laurent Viennot. Temporalizing multi-digraphs | Opening |
Registration |
Opening remarks | Dániel Marx. Constraint Satisfaction and Fixed-Parameter Tractability | |
| 09:05 | Invited talk: Karoliina Lehtinen. Where Büchi meets Parity | |||||
| 09:10 | Opening remarks | |||||
| 09:15 | Tutorial: Amar Hadzihasanovic. Combinatorics of higher-categorical diagrams I | Invited talk. Bernhard Aichernig. Learn to Test - Automata Learning for Formal Testing | ||||
| 09:30 | John Sylvester. Temporal exploration of random spanning tree models | Meet and greet | ||||
| 10:00 | Jessica Enright. Structural parameters for dense temporal graphs | Coffee break | ||||
| 10:30 | Coffee break | Tutorial: Amar Hadzihasanovic. Combinatorics of higher-categorical diagrams II | Loes Kruger, Sebastian Junges and Jurriaan Rot. Small Test Suites for Active Automata Learning | Vincent Moreau. A Fibrational Approach to Regular Languages of λ-terms | Andrei
Krokhin. A Theory of Gadget Reductions for CSPs |
Filip
Mazowiecki. Theoretical computer science: art or science? |
| 10:55 | Rick Koenders and Joshua Moerman. Output-decomposed Learning of Mealy Machines | |||||
| 11:00 | Thomas Erlebach. Parameterized Algorithms for Multi-Label Periodic Temporal Graph Realization | Kazuki
Watanabe. A Categorical Approach to Compositional Probabilistic Model
Checking |
Raheleh
Jalali. From Doubt to Determination: Building Confidence In Your PhD and
Beyond |
|||
| 11:15 | ||||||
| 11:20 | Matías Carrasco, Franz Mayr, Sergio Yovine, Johny Kidd, Martín Iturbide, Juan da Silva and Alejo Garat. Analyzing constrained LLM through PDFA-learning | |||||
| 11:30 | Nils Morawietz. Distance to Transitivity: New Parameters for Taming Reachability in Temporal Graphs | Nick Hu. Coherent invertibility in associative n-categories | Noam
Zeilberger. The Free Bifibration over a Functor |
Pawel
Sobocinski. How to give a talk |
||
| 11:45 | Hielke Walinga, Robert Baumgartner and Sicco Verwer. Database-assisted automata learning | Magnus
Wahlström. Sparsification and Running Time Aspects of CSPs |
||||
| 12:00 | Andrea Marino. On computing large temporal (unilateral) connected components | Matt
Earnshaw. Context-Free Languages of String Diagrams |
Mikołaj
Bojańczyk. Low level writing tips |
|||
| 12:10 | Daniele Dell'Erba, Yong Li and Sven Schewe. DFAMiner: Mining minimal separating DFAs from labelled samples | |||||
| 12:30 | ||||||
| 12:35 | Lunch | |||||
| 14:00 | Hendrik Molter. Realizing temporal transportation trees | Invited talk: Georg Struth. Single-set cubical categories and their formalisation with a proof assistant | Invited talk. Martin Berger. Dumb but fast >> smart and slow: fast grammar inference on GPUs | Marcin
Pilipczuk. Parametrized Complexity of CSPs Parameterized by the Number of
Unsatisfied Constraints |
Alex
Kavvos. Weak accept, or: how I learned to write papers and cope with
reviews |
|
| 14:05 | Invited
talk: Tarmo Uustalu. Sweedler Theory of Monads |
|||||
| 14:30 | Lutz Oettershagen. A higher-order temporal H-index for evolving networks | Niccolò
Veltri. Add a proof assistant to your toolbox |
||||
| 14:45 | Germán Vega, Michael Foster, Roland Groz, Neil Walkinshaw, Catherine Oriat and Adenilso Simão. Learning EFSM Models with Registers in Guards | Standa Živný. PTAS for CSPs from the Other Side | ||||
| 15:00 | George Skretas. How to reduce temporal cliques to find sparse spanners | Thomas
Seiller. Unifying algebraic lower bounds, semantically |
Karoliina
Lehtinen. Fantastic collaborations and where to find them: a beginner's guide
to conferences |
|||
| 15:05 | ||||||
| 15:10 | Robert Baumgartner and Sicco Verwer. PDFA Distillation via String Probability Queries | |||||
| 15:30 | ||||||
| 15:35 | Coffee break | |||||
| 16:00 | Dibyayan
Chakraborty. Algorithms and complexity for path covers of temporal DAGs: when is Dilworth dynamic? |
Clémence Chanavat. Diagrammatic sets as a model of homotopy types | Volodimir Mitarchuk and Rémi Eyraud. A Theoretical Analysis of the Incremental Counting Ability of LSTM in Finite Precision | Amirhossein
Akbar Tabatabai. Predicativism, Universality and Low-Complexity
Computation |
Paweł Rzążewski. CSPs for Children: Fine-Grained Complexity of the Graph Homomorphism Problem | Panel discussion. Ugo Dal Lago, Alex Kavvos, Karoliina Lehtinen, chaired by Marie Kerjean |
| 16:25 | Ekaterina Piotrovskaya, Leo Lobski and Fabio Zanasi. Learning Closed Signal Flow Graphs | |||||
| 16:30 | Antonio
Fernandez Anta. Nowcasting temporal trends using indirect surveys |
Peter
Hines. What is special about the 13th Permutoassociahedron? |
||||
| 16:45 | Open problem session | |||||
| 16:50 | Invited talk. Ryan Cotterell. TBA | |||||
| 17:00 | ||||||
| 17:35 | Closing remarks | |||||
| 17:55 | ||||||
Monday July 8 workshops
| TIME | LFMTP A242 |
TLLA A121 |
MSFP A224 |
| 09:00 | Carsten
Schürmann. Nominal State Separating Proofs |
Welcome | |
| 09:15 | Invited talk: Pierre-Marie Pédrot. Dialectica The Ultimate | ||
| 10:00 | Coffee break | ||
| 10:30 | Thomas
Traversié. Kuroda for Higher-Order Logic in the lambdaPi-Calculus Modulo
Theory |
Mikołaj Bojańczyk, Rafał Stefański. Function spaces for orbit-finite sets | Exequiel Rivas. Procontainers for Idioms, Arrows and Monads |
| 10:55 | Pedro Azevedo de Amorim. An enriched calculus for kernels and linear operators | ||
| 11:10 | Danel Ahman and Gašper Žajdela. A Stateful Time-Aware Operational Semantics for Temporal Resources | ||
| 11:15 | Rishikesh
Vaishnav. A Term-Patching Framework for Eliminating Definitional Equalities
in Lean |
||
| 11:20 | |||
| 11:45 | Thomas Seiller. An axiomatic presentation of linear realizability | ||
| 11:50 | Alexandre Garcia de Oliveira. Folds, Scans, and Moore Machines as Monoidal Profunctor Homomorphisms | ||
| 12:10 | Jacopo Furlan. The art of realizability | ||
| 12:30 | |||
| 12:35 | Lunch | ||
| 14:00 | Thomas Traversié.
Proofs for Free in the lambdaPi-Calculus Modulo Theory |
Tutorial: Nobuko Yoshida. Session types, Linear Logic and Expressiveness | Zachary Flores, Angelo Taranto, Yakir Forman and Eric Bond. Formalizing Operads for a Categorical Framework of DSL Composition |
| 14:30 | Chad Nester and Niels Voorneveld. Protocol Choice and Iteration for the Free Cornering | ||
| 14:45 | Gabriele
Cecilia and Alberto Momigliano. A Beluga Formalization of the Harmony Lemma
in the pi-Calculus |
||
| 15:00 | Zev Shirazi. Commutative Codensity Monads and Probability Bimeasures | ||
| 15:30 | Coffee break | ||
| 16:00 | Terrance
Gray, Gopalan Nadathur. Binding Contexts as Partitionable Multisets in
Abella |
Davide Barbarossa. Stability property for the Call-by-Value lambda-calculus through Taylor expansion | Exequiel Rivas and Tarmo Uustalu. Concurrent Monads for Shared State |
| 16:25 | Raffaele Di Donna. Injectivity of the coherent model for a fragment of connected MELL proof-nets | ||
| 16:30 | Invited talk. Nathan Corbyn. Understanding the Classical Monad-Theory Correspondence | ||
| 16:45 | Florian Guthmann, Philip Kaludercic, Johannes
Lindner, Tadeusz Litak. Abella2Coq: Translating Abella Specifications into
Coq |
||
| 16:50 | Giulio Guerrieri. The theory of meaningfulness in the Call-by-Value lambda-calculus | ||
| 17:15 | Closure | ||
| 17:25 | |||
Monday July 8 morning invited talk
| TIME | LICS INVITED
TALK (Chair: Ugo Dal Lago) Auditorium Maximum - A002 |
| 09:00 | Alexandra Silva.Semirings in Logic, Semantics, and Verification. |
| Abstract.Semirings are a fundamental algebraic structure. In this talk, I will discuss how semirings appear in different places in the semantics of programming languages, program logics, and verification. I will showcase their importance through recent work on Outcome Logic and Kleene Algebra. | |
| 09:55 |
Monday July 8 morning regular session
| TIME | LICS S1 -
MODAL, TEMPORAL, HIGHER ORDER AND COUNTING LOGICS (Chair: Karoliina Lehtinen) Auditorium Maximum - A002 |
LICS S2 -
CATEGORY THEORY (Chair: Samuel Mimram) A543 |
ICALP A1 -
SPARSIFICATION AND CUTS (Chair: Parinya Chalermsook) A325 |
ICALP A2 -
COMPLEXITY THEORY 1 (Chair: Bruno Loff) Tallinn Hall - M218 |
| 10:30 | Bharat Adsul, Paul Gastin, Shantanu Kulkarni and Pascal Weil.
An expressively complete local past propositional dynamic logic over
Mazurkiewicz traces and its applications |
Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon and Pawel Sobocinski. Diagrammatic Algebra of First-order Logic | Yotam Kenneth and Robert Krauthgamer. Cut Sparsification and Succinct Representation of Submodular Hypergraphs | Guy Goldberg. Linear Relaxed Locally Decodable and Correctable Codes Do Not Need Adaptivity and Two-Sided Error |
| 10:45 | Valérie
Berthé, Toghrul Karimov, Joris Nieuwveld, Joel Ouaknine, Mihir
Vahanwala and James Worrell. On the Decidability of Monadic
Second-Order Logic with Arithmetic Predicates (distinguished paper) |
Masahito Hasegawa and Serge Lechenne. Braids, Twists, Trace and Duality in Combinatory Algebras | ||
| 10:55 | Sanjeev Khanna, Aaron Putterman and Madhu Sudan. Almost-Tight Bounds on Preserving Cuts in Classes of Submodular Hypergraphs | Xin Li and Yan Zhong. Two-Source and Affine Non-Malleable Extractors for Small Entropy | ||
| 11:00 | Maximilian Pflueger, Johannes Marti and Egor V. Kostylev. A Characterisation Theorem for Two-Way Bisimulation-Invariant Monadic Least Fixpoint Logic Over Finite Structures | Philip Saville and Hugo Paquet. Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads | ||
| 11:15 | Miroslav
Chodil and Antonin Kucera. The Finite Satisfiability Problem for
PCTL is Undecidable (distinguished paper) |
Nihil Shah and Amin Karamlou. Directed Containers That Do Not Distribute Over Distribution Monads | ||
| 11:20 | Orestis Plevrakis, Seyoon Ragavan and S. Matthew Weinberg. On the cut-query complexity of approximating max-cut | Hamed Hatami, Kaave Hosseini, Shachar Lovett and Anthony Ostuni. Refuting approaches to the log-rank conjecture for XOR functions | ||
| 11:30 | Piotr Ostropolski-Nalewaja and Tim Lyon. Decidability of Quasi-Dense Modal Logics | Zeinab Galal and Jean-Simon Pacaud Lemay. Combining fixpoint and differentiation theory | ||
| 11:45 | Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos and Alexandre Vigny. Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes | Eric Finster, Alex Rice and Jamie Vicary. A Syntax for Strictly Associative and Unital ∞-Categories | Agastya Vibhuti Jha and Akash Kumar. A Sublinear Time Tester for Max-Cut on Clusterable Graphs | Vladimir Podolskii and Dmitrii Sluch. One-Way Communication Complexity of Partial XOR Functions |
| 12:00 | Sandra Kiefer and Daniel Neuen. Bounding the Weisfeiler--Leman Dimension via a Depth-Analysis of I/R-Trees | Thorsten Wißmann and Stefan Milius. Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda | ||
| 12:10 | Surender Baswana and Koustav Bhanja. Vital Edges for (s,t)-mincut: Efficient Algorithms, Compact Structures, & Optimal Sensitivity Oracles | Vikraman Arvind and Pushkar Joglekar. A Multivariate to Bivariate Reduction for Noncommutative Rank and Related Results | ||
| 12:15 | Martin Grohe and Eran Rosenbluth. Are Targeted Messages More Effective? | Mayuko Kori, Kazuki Watanabe, Jurriaan Rot and Shin-Ya Katsumata. Composing Codensity Bisimulations | ||
| 12:25 |
Monday July 8 afternoon invited session
| TIME | LICS INVITED
TUTORIAL (Chair: Pawel Sobocinski) Europe Hall - A222 |
ICALP INVITED
TALK (Chair: Ola Svensson) Auditorium Maximum - A002 |
| 14:00 | Alex Simpson.A tutorial on Sheaf Semantics. | Danupon Nanongkai.Cross-Paradigm Graph Algorithms. |
| Abstract. Sheaf semantics provides a unifying framework for modelling
intuitionistic, intermediate and classical logics. On the one hand, it
seamlessly generalises several more specific forms of semantics such as the
Kripke and Beth models of intuitionistic logic, as well as Cohen's forcing
interpretation of classical logic (as used in his set-theoretic independence
proofs). On the other, it naturally embraces some genuinely new types of
model in which the underlying structure of "possible worlds" or "conditions"
is given by a category rather than a partial order. Starting with the Kripke semantics of intuitionistic logic, I shall build towards the goal of presenting and explaining sheaf semantics in its general form, together with example applications. While the core technical content of the tutorial dates back some 50 years to the 1970s, the technology of sheaf semantics remains relevant today, with several current applications in logic in computer science. The aim is to make the tutorial intelligible to an audience who have some general knowledge of logic, but potentially no prior background in category theory. |
Abstract. A goal of the theory of
graph algorithms is algorithmic techniques that enable computing devices to
process graph data with little resources (time, space, communication
overhead, etc.). This led to extensive studies of graph algorithms in various
models of computation (sequential algorithms, distributed algorithms,
streaming algorithms, etc.) by many sub-communities. "Cross-paradigm
graph algorithms" is an effort to attack the same problem in many models
of computation simultaneously, intending to generate new insights that may
not emerge from the isolated viewpoint of a single model and to ultimately
develop techniques that can be used to solve graph problems near-optimally
across many models of computation.
In this talk, I will discuss some recent
advances in graph algorithmic techniques for basic graph problems (e.g.
minimum cut, shortest path, and maximum flow) in connection to this research
program, especially some insights that led to cross-paradigm algorithms and
to answering notorious open questions.
No background will be assumed from the audience beyond familiarity with textbook graph algorithms. |
|
| 15:00 | ||
| 15:25 |
Monday 8 July afternoon regular session
| TIME | LICS S3 -
TOPICS IN LOGIC, REWRITING, AND PROOF THEORY (Chair: Alex Simpson) Auditorium Maximum - A002 |
ICALP A3 -
APPROXIMATION ALGORITHMS I (Chair: Andreas Emil Feldmann) Europe Hall - A222 |
ICALP A4 -
PARAMETRIZED ALGORITHMS I (Chair: Bart Jansen) A543 |
ICALP A5 -
HARDNESS OF APPROXIMATION (Chair: Parinya Chalermsook) A325 |
| 16:00 | Anupam Das and Abhishek De. A proof theory of right-linear (omega-)grammars via cyclic proofs | Sami Davies, Benjamin Moseley and Heather Newman. Simultaneously Approximating All lp-norms in Correlation Clustering | Esther Galby, Sándor Kisfaludi-Bak, Dániel Marx and Roohani Sharma. Subexponential Parameterized Directed Steiner Network Problems on Planar Graphs: a Complete Classification | Noga Ron-Zewi and Elie Abboud. Finer-grained Reductions in Fine-grained Hardness of Approximation |
| 16:15 | Victor Arrial, Giulio Guerrieri and Delia Kesner. Genericity Through Stratification | |||
| 16:25 | Niklas Schlomberg. An improved integrality gap for disjoint cycles in planar graphs | Robert Ganian, Haiko Müller, Sebastian Ordyniak, Giacomo Paesani and Mateusz Rychlicki. A Tight Subexponential Algorithm for Two-Page Book Embedding | Shuangle Li, Bingkai Lin and Yuwei Liu. Improved Lower Bounds for Approximating Parameterized Nearest Codeword and Related Problems under ETH | |
| 16:30 | Chris Barrett, Willem Heijltjes and Daniel Castle.The Relational Machine Calculus | |||
| 16:45 | Fabian Mitterwallner, Aart Middeldorp and René Thiemann. Linear Termination is Undecidable | |||
| 16:50 | Yu Chen and Zihan Tan. Lower Bounds on 0-Extension with Steiner Nodes | Boris Klemz and Marie Diana Sieper. Constrained Level Planarity is FPT with Respect to the Vertex Cover Number | Naoto Ohsaka. Alphabet Reduction for Reconfiguration Problems | |
| 17:00 | Marie
Kerjean and Pierre-Marie Pédrot. ∂ is for Dialectica (distinguished paper) |
|||
| 17:15 | Cameron Allett. Non-Elementary Compression of First-Order Proofs in Deep Inference Using Epsilon-Terms | Fateme Abbasi, Marek Adamczyk, Miguel Bosch Calvo, Jarosław Byrka, Fabrizio Grandoni, Krzysztof Sornat and Antoine Tinguely. An O(loglog n)-Approximation for Submodular Facility Location | Matthias Bentert, Pål Grønås Drange, Fedor V. Fomin, Petr A. Golovach and Tuukka Korhonen. Two-sets cut-uncut on planar graphs | Shuichi Hirahara and Naoto Ohsaka. Optimal PSPACE-hardness of Approximating Set Cover Reconfiguration |
| 17:30 | Raheleh Jalali and Stefan Hetzl. On the Completeness of Interpolation Algorithms | |||
| 17:40 | Reut Levi, Talya Eden and Dana Ron. Testing Ck-freeness in bounded-arboricity graphs | Argyrios Deligkas, Eduard Eiben, Robert Ganian, Iyad Kanj and Ramanujan M. Sridharan. Parameterized Algorithms for Coordinated Motion Planning: Minimizing Energy | Omkar Baraskar, Agrim Dewan, Chandan Saha and Pulkit Sinha. NP-hardness of testing equivalence to sparse polynomials and constant support polynomials | |
| 17:45 | Søren Brinck Knudstorp. Relevant S is Undecidable | |||
| 17:55 |
Tuesday July 9 workshops
| TIME | IWC A224 |
TLLA A121 |
ITRS A242 |
WOMEN IN LOGIC Europe Hall - A222 |
| 09:00 | Invited talk: Aart Middeldorp. Confluence of Logically Constrained Rewrite Systems | Welcome | Manon Blanc. The domino problem is decidable for robust tilesets | |
| 09:10 | Invited talk: Andrej Dudenhefner. From Normalization to Typability via Subject Expansion | |||
| 09:15 | Tutorial: Davide Barbarossa. Differential aspects of the approximation theory of the lambda-calculus I | Saina Sunny. Deciding Conjugacy of a Rational Relation | ||
| 09:30 | C Aiswarya. On the Satisfiability of Context-free String Constraints with Subword-Ordering and Transduction | |||
| 09:45 | Zeynep Senahan Yildiz. A scalable resolution method for exact entailment | |||
| 10:00 | Coffee break | |||
| 10:30 | Misaki Kojima and Naoki Nishida. On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs | Tutorial: Davide Barbarossa. Differential aspects of the approximation theory of the lambda-calculus II | Miguel Ramos: Non-Idempotent Intersection Types for Global State | Chana Weil-Kennedy. A Uniform Framework for Language Inclusion Problems |
| 10:45 | Kinnari Dave. Combining Quantum and Classical Control | |||
| 10:50 | Beniamino Accattoli, Giulio Guerrieri and Maico Leberle: Strong Call-by-Value and Multi Types | |||
| 11:00 | Salvador
Lucas. From Subtree Replacement Systems to Term Rewriting Systems: a Roadmap
to Orthogonality |
Žaneta Semanišinová. Classification Transfer for CSPs via Algebraic Products | ||
| 11:15 | Stefano Catozi. Normalization in multiplicative exponential linear logic via Taylor expansion | Victor Arrial: Call-by-Value Typing Revisited, for Free? | Ana Clara Rezende. Interpretations of the logic of FDE in terms of information and evidence | |
| 11:30 | Vincent van Oostrom. The problem of the calissons, by rewriting | Nina Pardal. A logic-based framework for database repairs | ||
| 11:35 | ||||
| 11:40 | ||||
| 11:45 | Joint
IITRS/TLLA Invited talk: Giulio Manzonetto. Coloring Intersection Types (A121) |
Invited
talk: Sandra Kiefer. Constructive Interactions |
||
| 12:00 | Salvador
Lucas. A Roadmap to Orthogonality of Conditional Term Rewriting Systems |
|||
| 12:30 | Lunch | |||
| 14:00 | Ievgen Ivanov. On
Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract
Rewriting Systems |
Wesley Fussner, Simon Santschi. Interpolation in extensions of linear logic | Joint ITRS/Women In Logic Invited talk: Viviana Bono. Types for
(Slow) AI (Europe Hall - A222) |
|
| 14:25 | Niccolò Veltri, Cheng-Syuan Wan. Craig interpolation for semi-substructural logics | |||
| 14:30 | Aart
Middeldorp. CoCo 2024 |
|||
| 14:45 | Ana
Catarina Sousa. Partial proof terms in the study of proof search |
|||
| 14:50 | ||||
| 15:00 | Luis Caires. On expressing stateful computation in linear logic | Adrienne Lancelot. Separating Terms through Multi Types | Filipa Mendes. The logical essence of call-by-name CPS translations | |
| 15:15 | Daniella
Santaguida. Nominal Equational Reasoning |
|||
| 15:25 | Business meeting | Coffee break | ||
| 15:30 | ||||
| 16:00 | Salvador
Lucas. Orthogonality of Generalized Term Rewriting Systems |
Marie Kerjean. Laplace transformation and symmetry in differential linear logic | Joseph Paulus, Daniele Nantes-Sobrinho and Jorge A. Pérez. Intersection Types Meet Session Types | Invited
talk: Amal Ahmed. New Techniques for Sound Language Interoperability |
| 16:25 | Morgan Rogers. A supply of functorial models of linear logic | Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro and Betti Venneri. YACC: Yet Another Church Calculus | ||
| 16:30 | Thiago
Felicissimo. Second-order Church-Rosser modulo, without normalization |
|||
| 16:45 | Round Table: Kait O'Neil & Greta Yorsh. Women in industry and academia | |||
| 16:50 | Closure | Pablo Barenbaum, Eduardo Bonelli and Mariana Milicich. Intersection Types as Evaluation Types | ||
| 17:00 | Nao
Hirokawa and Kiraku Shintani. Rule Removal for Confluence |
|||
| 17:10 | Aleksy Schubert. Modest annotations with intersection types | |||
| 17:30 | Vincent van Oostrom. Confluence by the
Z-property for De Bruijn's lambda-calculus with nameless dummies, based on
PLFA |
|||
| 17:35 | Abhishek De, Charles Grellois, Lê Thành Dũng Nguyễn and Cécilia Pradic. Higher-order model checking meets implicit automata: Finitary colored semantics of infinitary λ-terms | |||
| 17:55 | ||||
Tuesday 9 July morning invited talk
| TIME | ICALP INVITED
TALK (Chair: Martin Grohe) Auditorium Maximum - A002 |
| 09:00 | Anuj Dawar. Limits of Symmetric Computation. |
| I survey recent work on symmetric computation. A number of strands of work, from logic, circuit complexity, combinatorial optimization and other areas have converged on similar notions of symmetry in computation. I talk about how methods for showing inexpressibility in logic translate into lower bounds for symmetric models of computation. I illustrate this with applications in algebraic circuit complexity. I also discuss perspectives for future work. | |
| 09:55 |
Tuesday 9 July morning regular session
| TIME | LICS S4 - TYPE
THEORY (Chair: Martín Escardó) Auditorium Maximum - A002 |
ICALP B1 -
AUTOMATA (Chair: Antonin Kucera) Tallinn Hall - M218 |
ICALP A6 -
PARAMETRIZED ALGORITHMS II (Chair: Thore Husfeldt) A543 |
ICALP A7 -
CONTINUOUS OPTIMIZATION (Chair: Kent Quanrud) A325 |
ICALP A8 -
MIXED GRAPH PROBLEMS (Chair: Amit Kumar) A046 |
| 10:30 | Pierre-Marie
Pédrot. “Upon This Quote I Will Build My Church Thesis” (distinguished paper) |
Arnaud Carayol and Lucien Charamond. The structure of trees in the pushdown hierarchy | Florent Foucaud, Esther Galby, Liana Khazaliya, Shaohua Li, Fionn Mc Inerney, Roohani Sharma and Prafullkumar Tale. Problems in NP can Admit Double-Exponential Lower Bounds when Parameterized by Treewidth and Vertex Cover | Emile Anand, Jan van den Brand, Mehrdad Ghadiri and Daniel J Zhang. The Bit Complexity of Dynamic Algebraic Formulas and their Determinants | Shyan Akmal, Virginia Vassilevska Williams and Nicole Wein. Detecting Disjoint Shortest Paths in Linear Time and More |
| 10:45 | Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli. Separating Markov's Principles | ||||
| 10:55 | Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero and Adriano Peron. Automata-Theoretic Characterisations of Branching-Time Temporal Logics | Baris Can Esmer, Jacob Focke, Dániel Marx and Paweł Rzążewski. Fundamental Problems on Bounded-Treewidth Graphs: The Real Source of Hardness | Li Chen and Mingquan Ye. High-Accuracy Multicommodity Flows via Iterative Refinement | Mohammad Hossein Bateni, Laxman Dhulipala, Kishen Gowda, D Ellis Hershkowitz, Rajesh Jayaram and Jakub Łącki. It's Hard to HAC with Average Linkage! | |
| 11:00 | Kirstin Peters and Nobuko Yoshida. Separation and Encodability in Mixed Choice Multiparty Sessions | ||||
| 11:15 | Christian Sattler and David Wärn. Natural numbers from integers | ||||
| 11:20 | Julian Dörfler and Christian Ikenmeyer. Functional Closure Properties of Finite N-weighted Automata | Clément Dallard, Fedor Fomin, Petr Golovach, Tuukka Korhonen and Martin Milanič. Computing Tree Decompositions with Small Independence Number | Cella Florescu, Rasmus Kyng, Maximilian Probst Gutenberg and Sushant Sachdeva. Optimal Electrical Oblivious Routing on Expanders | Mario Grobler, Stephanie Maaz, Nicole Megow, Amer Mouawad, Vijayaragunathan Ramamoorthi, Daniel Schmand and Sebastian Siebertz. Solution discovery via reconfiguration for problems in P | |
| 11:30 | Samuel Mimram and Emile Oleon. Delooping cyclic groups with lens spaces in homotopy type theory | ||||
| 11:45 | Ulrik Buchholtz and Johannes Schipp von Branitz. Primitive Recursive Dependent Type Theory | Paul Gallot, Sebastian Maneth, Keisuke Nakano and Charles Peyrat. Deciding Linear Height and Linear Size-to-Height Increase of Macro Tree Transducers | Andreas Emil Feldmann and Michael Lampis. Parameterized Algorithms for Steiner Forest in Bounded Width Graphs | Sushant Sachdeva, Anvith Thudi and Yibin Zhao. Better Sparsifiers for Directed Eulerian Graphs | Johannes Meintrup, Frank Kammer, Konstantinos Dogeas, Thomas Erlebach and William K. Moses Jr.. Exploiting Automorphisms of Temporal Graphs for Fast Exploration and Rendezvous |
| 12:00 | Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus and Marc Bezem. On symmetries of spheres in univalent foundations | ||||
| 12:10 | C. Aiswarya, Amaldev Manuel and Saina Sunny. Edit Distance of Finite State Transducers | Narek Bojikian and Stefan Kratsch. A tight Monte-Carlo algorithm for Steiner Tree parameterized by clique-width | Kevin Hua, Daniel Li, Jaewoo Park and Thatchaphol Saranurak. Finding Most Shattering Minimum Vertex Cuts of Polylogarithmic Size in Near-Linear Time | Augusto Modanese and Yuichi Yoshida. Testing Spreading Behavior in Networks with Arbitrary Topologies | |
| 12:15 | Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Declassification Policy for Program Complexity Analysis | ||||
| 12:25 |
Tuesday 9 July lunch steering committee meetings
LiCS steering committee meeting - A046
ICALP steering committee meeting - A007
Tuesday 9 July afternoon regular session
| TIME | LICS S5 -
PROBABILISTIC AND QUANTUM COMPUTATION (Chair: Pierre Clairambault) Auditorium Maximum - A002 |
ICALP B2 -
INFINITE-STATE SYSTEMS (Chair: Karoliina Lehtinen) Tallinn Hall - M218 |
ICALP A9 -
MATROIDS (Chair: Fabrizio Grandoni) A325 |
ICALP A10 -
COMPLEXITY THEORY II (Chair: Bruno Loff) A543 |
ICALP A11 -
GRAPH THEORY (Chair: Daniel Marx) A046 |
| 14:00 | Alex
Simpson. Equivalence and Conditional Independence in Atomic Sheaf Logic (distinguished paper) |
Sylvain Schmitz and Lia Schütze. On the Length of Strongly Monotone Descending Chains over ℕᵈ | Kent Quanrud. Adaptive sparsification for matroid intersection | Zhenjian Lu and Rahul Santhanam. Impagliazzo’s Worlds Through the Lens of Conditional Kolmogorov Complexity | Andreas Björklund, Petteri Kaski and Jesper Nederlof. Another Hamiltonian cycle in bipartite Pfaffian graphs |
| 14:15 | John Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed and Steven Holtzen. A Nominal Approach to Probabilistic Separation Logic | ||||
| 14:25 | George Kenison. The Threshold Problem for Hypergeometric Sequences with Quadratic Parameters | Yusuke Kobayashi and Tatsuya Terao. Subquadratic Submodular Maximization with a General Matroid Constraint | Jonas Kamminga and Sevag Gharibian. BQP, meet NP: Search-to-decision reductions and approximate counting | Kristóf Bérczi, Karthekeyan Chandrasekaran, Tamás Király and Shubhang Kulkarni. Splitting-off in Hypergraphs | |
| 14:30 | Victor Blanchi and Hugo Paquet. Element-free probability distributions and random partitions | ||||
| 14:45 | James Hefford and Matt Wilson. A Profunctorial Semantics for Quantum Supermaps | ||||
| 14:50 | Pavol Kebis, Florian Luca, Joel Ouaknine, Andrew Scoones and James Worrell. On Transcendence of Numbers Related to Sturmian and Arnoux-Rauzy Words | Florian Hörsch, András Imolay, Ryuhei Mizutani, Taihei Oki and Tamás Schwarcz. Problems on Group-labeled Matroid Bases | Shalev Ben-David and Srijita Kundu. Oracle separation of QMA and QCMA with bounded adaptivity | Édouard Bonnet, Julien Duron, John Sylvester, Viktor Zamaraev and Maksim Zhukovskii. Tight Bounds on Adjacency Labels for Monotone Graph Classes | |
| 15:00 | Pietro Di Gianantonio and Abbas Edalat. A Cartesian Closed Category for Random Variables | ||||
| 15:15 | Wojciech Różowski and Alexandra Silva. A Completeness Theorem for Probabilistic Regular Expressions | Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine and James Worell. The 2-Dimensional Constraint Loop Problem is Decidable | Tanmay Inamdar, Pallavi Jain, Daniel Lokshtanov, Abhishek Sahu, Saket Saurabh and Anannya Upasana. Satisfiability to Coverage in Presence of Fairness, Matroid, and Global Constraints | Michaela Borzechowski, John Fearnley, Spencer Gordon, Rahul Savani, Patrick Schnider and Simon Weber. Two Choices are Enough for P-LCPs, USOs, and Colorful Tangents | Martin Grohe and Daniel Neuen. Isomorphism for Tournaments of Small Twin Width |
| 15:30 | Alexandre Clément, Noé Delorme and Simon Perdrix. Minimal Equational Theories for Quantum Circuits | ||||
| 15:40 | Raphael Douglas Giles, Vincent Jackson and Christine Rizkallah. T-Rex: Termination of Recursive Functions using Lexicographic Linear Combinations | Ilan Doron-Arad, Ariel Kulik and Hadas Shachnai. Lower Bounds for Matroid Optimization Problems with a Linear Constraint | Yiannis Giannakopoulos, Alexander Grosz and Themistoklis Melissourgos. On the Smoothed Complexity of Combinatorial Local Search | ||
| 15:45 | Lorenzo Ciardo. Quantum advantage and CSP complexity | ||||
| 15:55 |
Tuesday 9 July afternoon special session
Live broadcast on YouTube.
| TIME | AWARD TALKS Auditorium Maximum - A002 |
| 16:30 | Gödel Prize. (Chair: Mikołaj Bojańczyk) Ryan Williams. Circuit Complexity from Circuit Analysis Algorithms |
| I will explain on a personal level how I got into circuit complexity, and how I ended up proving circuit lower bounds like "NEXP does not have polynomial-size ACC circuits". In short, my path to circuit complexity lower bounds was circuitous, arising from the study of exact exponential time algorithms. I'll also speak about what else has been proved since the initial results, building on the various ideas that were introduced. | |
| 17:30 | LiCS ToT. (Chair: Franz Baader) Samson Abramsky and Bob
Coecke. A categorical semantics of quantum
protocols. This extraordinary paper has had a major impact on the development of quantum computation in the logic and computation community. It has led to new algebraic and diagrammatic ways of thinking about quantum computation and has stimulated research on quantum programming languages, calculi for reasoning about quantum computation, and lately even error correction. Using the \emph{logic of compact closed categories}, the paper gives an abstract treatment of fundamental aspects of quantum mechanics and quantum computation, with only sparse use of the usual mathematical machinery (such as linear algebra and Hilbert spaces). It shows that major protocols of quantum computation, such as teleportation and entanglement swapping, can not only be formulated, but also proved to be correct in this framework. Fundamental aspects of quantum mechanics are given an abstract treatment, most notably the Born rule. In summary, this paper began and gave impetus to the development of an abstract way to reason about quantum mechanics and quantum computation. It is very highly cited and has had major impact on reasoning about quantum computation and quantum mechanics. |
| 17:40 | LiCS ToT. (Chair: Franz Baader) Andreas Podelski and
Andrey Rybalchenko. Transition Invariants. The paper presents in a very clean and elegant way a general characterization of the validity of liveness properties of programs, like termination and other such properties expressed in temporal logic. This is achieved by employing relations over program states, called transition invariants, which contain the transitive closure of the state transition relation defined by the program. The key result is that the absence of infinite executions can be reduced to proving that the transition invariant is a finite union of well-founded relations. The authors show how to use such disjunctively well-founded transition invariants to validate temporal properties of concurrent systems. The paper has greatly influenced the development of techniques and tools for proving termination of programs automatically since it nicely combines the use of disjunctive well-foundedness with the construction of an abstraction of the program transition relation, which is the transition invariant. The suitability for automation of the approach has been crucial in its success. In addition, the paper also had a large impact on the design of powerful techniques based on termination analysis to (dis)prove a great variety of temporal properties of programs. |
| 17:50 | Presburger award. Justin Hsu. Logics for Separation in Randomized Programs. |
| Separation logic is a well-studied and practically impactful technique for reasoning about sharing and separation in programs with complex behavior, such as memory allocation or concurrency. In this talk, I'll give a brief tour of recent work generalizing these methods to randomized programs and probabilistic notions of separation. | |
| 18:10 | Presburger award. Pravesh Kothari. Semirandom Optimization and Applications |
| Semirandom input models are a hybrid between benign average-case and adaptive adversarial choice of inputs. They were introduced in the 1990s to escape the strong NP-hardness of approximation of worst-case instances without overfitting to the quirks of a specific random model. In this talk, I will briefly discuss recent progress in designing algorithms for semirandom models of foundational NP-hard problems with guarantees matching the best-known results for well-studied vanilla random models. I will also discuss some surprising applications of the resulting techniques in resolving long-studied questions in extremal combinatorics, local error correcting codes, and additive number theory. | |
| 18:25 |
Wednesday 10 July morning invited talk
| TIME | LICS/ICALP/FSCD
JOINT INVITED TALK (Chair: Tarmo Uustalu) Auditorium Maximum - A002 |
| 09:00 | Stephanie Weirich. Tracking how dependently typed functions use their arguments. |
| Abstract. Dependent type systems extend the expressiveness of typed
programming languages by allowing the result types of functions to depend on
the values of their arguments. This feature allows programmers to design
expressive interfaces and express application-specific properties about their
code. However, many function arguments in these languages are purely
specificational: they are there to provide information to the type checker,
but they otherwise have no runtime significance. These arguments can be identified
through various mechanisms, such as usage analysis (counting how many times
functions use their parameters) or dependency analysis (tracking which
results depend on which inputs). In this talk, I will show how dependent-type
systems can integrate such analyses and make use of this information while
checking programs. |
|
| 09:55 |
Wednesday 10 July morning regular session
| TIME | LICS S6 - FIRST
ORDER LOGIC (Chair: Sławomir Lasota) Auditorium Maximum - A002 |
FSCD S1 -
HOMOTOPY TYPE THEORY (Chair: Pierre-Marie Pedrot) Europe Hall - A222 |
ICALP B3 -
SEMANTIC MODELLING AND VERIFICATION (Chair: Andrzej Murawski) Tallinn Hall - M218 |
ICALP A12 -
GRAPH DISTANCE PROBLEMS (Chair: Giuseppe F. Italiano) A543 |
ICALP A13 -
STRING AND MIXED PROBLEMS (Chair: Seth Pettie) A325 |
| 10:30 | Jakub Gajarský, Michał Pilipczuk, Szymon Toruńczyk, Giannos Stamoulis and Marek Sokołowski. Elementary first-order model checking for sparse graphs | Maximilian Doré, Evan Cavallo and Anders Mörtberg. Automating Boundary Filling in Cubical Agda | Cheng Zhang, Arthur Azevedo de Amorim and Marco Gaboardi. Domain Reasoning In TopKAT | Shiri Chechik and Tianyi Zhang. Faster Algorithms for Dual-Failure Replacement Paths | Itai Boneh, Shay Golan, Shay Mozes and Oren Weimann. Õptimal Dynamic Time Warping on Run-Length Encoded Strings |
| 10:45 | Tal Hershko and Maksim Zhukovskii. First order distinguishability of sparse random graphs | ||||
| 10:55 | Go Hashimoto, Daniel Gaina and Ionuț Țuțu. Forcing, Transition Algebras, and Calculi | Shiri Chechik and Tianyi Zhang. Path-Reporting Distance Oracles with Logarithmic Stretch and Linear Size | Panagiotis Charalampopoulos, Pawel Gawrychowski and Samah Ghazawi. Optimal Bounds for Distinct Quartics | ||
| 11:00 | Oskar Fiuk, Emanuel Kieronski and Vincent Michielini. On the complexity of Maslov’s class K | Camil Champin, Samuel Mimram and Oleon Emile. Delooping generated groups in homotopy type theory | |||
| 11:15 | Danila
Demin and Maksim Zhukovskii. First order complexity of finite random
structures (distinguished paper) |
||||
| 11:20 | Wojciech Różowski. A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions | Ariel Korin, Tsvi Kopelowitz and Liam Roditty. On the Space Usage of Approximate Distance Oracles with Sub-2 Stretch | Nick Fischer and Leo Wennmann. Minimizing Tardy Processing Time on a Single Machine in Near-Linear Time | ||
| 11:30 | Nadim Kasymov, Nadira Karimova and Bakh Khoussainov. Defining algorithmically presented structures in first order logic | Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion | |||
| 11:40 | |||||
| 11:45 | Nathan Lhote, Vincent Michielini and Michał Skrzypczak. Uniformisation of Regular Relations in First-Order Logic with Two Variables | Mikołaj Bojańczyk, Lê Thành Dũng Nguyên and Rafał Stefański. Function spaces for orbit-finite sets | Greg Bodwin, Gary Hoppenworth, Virginia Vassilevska Williams, Nicole Wein and Zixuan Xu. Additive Spanner Lower Bounds with Optimal Inner Graph Structure | Andrei Constantinescu, Pascal Lenzner, Rebecca Reiffenhäuser, Daniel Schmand and Giovanna Varricchio. Solving Woeginger’s Hiking Problem: Wonderful Partitions in Anonymous Hedonic Games | |
| 12:00 | Harry Vinall-Smeeth. From Quantifier Depth to Quantifier Number: Separating Structures with k Variables | Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru and Jamie Vicary. homotopy.io: a proof assistant for finitely-presented globular n-categories | |||
| 12:10 | Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger and Chana Weil-Kennedy. Verification of Population Protocols with Unordered Data | Greg Bodwin, Chengyuan Deng, Jie Gao, Gary Hoppenworth, Jalaj Upadhyay and Chen Wang. The Discrepancy of Shortest Paths | Lucas Gretta and Eric Price. Sharp Noisy Binary Search with Monotonic Probabilities | ||
| 12:15 | Thomas Place and Marc Zeitoun. Dot-depth three, return of the J-class | ||||
| 12:25 |
Wednesday 10 July afternoon regular session
| TIME | LICS S7 - GAMES
AND PROGRAM SEMANTICS (Chair: Andrzej Murawski) Tallinn Hall - M218 |
FSCD S2 -
CATEGORIES (Chair: Niels van der Weide) Europe Hall - A222 |
ICALP BEST
PAPERS Auditorium Maximum - A002 (Chair: Martin Grohe) |
| 14:00 | Ali Asadi, Krishnendu Chatterjee, Jakub Svoboda and Raimundo Saona Urmeneta. Deterministic Sub-exponential Algorithm for Discounted-sum Games with Unary Weights | Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva and Fabio Zanasi. A Categorical Approach to DIBI Models | Ce Jin and Hongxun Wu. A Faster Algorithm for Pigeonhole Equal Sums |
| 14:15 | Noah Abou El Wafa and André Platzer. Complete Game Logic with Sabotage | ||
| 14:20 | |||
| 14:25 | Kingsley Yung. Limits of Sequential Local Algorithms on the Random k-XORSAT Problem | ||
| 14:30 | Sougata Bose, Rasmus Ibsen-Jensen and Patrick Totzke. Bounded-Memory Strategies in Partial-Information Games | Ralph Matthes, Kobe Wullaert and Benedikt Ahrens. Substitution for non-wellfounded syntax with binders through monoidal categories | |
| 14:45 | Antonio Casares and Pierre Ohlmann. Positional ω-regular languages | ||
| 14:50 | Yuda Feng and Shi Li. A Note on Approximating Weighted Nash Social Welfare with Additive Valuations | ||
| 15:00 | Yoàv Montacute and Glynn Winskel. Concurrent Games over Relational Structures: The Origin of Game Comonads | Jean-Simon Lemay and Marie Kerjean. Laplace Distributors and Laplace Transformations for Differential Categories | |
| 15:15 | Vasileios Koutavas, Yu-Yang Lin and Nikos Tzevelekos. Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence | Dmitry Chistikov, Alessio Mansutti and Mikhail Starchak. Integer Linear-Exponential Programming in NP by Quantifier Elimination | |
| 15:30 | Pierre Clairambault and Simon Forest. An Analysis of Symmetry in Quantitative Semantics | Benoît Guillemet, Matthieu Piquerez and Assia Mahboubi. Machine-Checked Categorical Diagrammatic Reasoning | |
| 15:40 | Roland Guttenberg. Flattability of Priority Vector Addition Systems | ||
| 15:45 | Sergey Goncharov, Stefan Milius, Stelios Tsampas and Henning Urbat. Bialgebraic Reasoning on Higher-order Program Equivalence | ||
| 15:55 |
Wednesday 10 July afternoon special session
| TIME | LICS INVITED
TUTORIAL (Chair: Bruce Kapron) A543 |
FSCD INIVITED
TALK (Chair: Jakob Rehof) Europe Hall - A222 |
AWARD TALKS
& EATCS BUSINESS Auditorium Maximum - A002 Live broadcast |
| 16:30 | Sam Buss. Provability, totality, and complexity in bounded arithmetic. | Roderick Bloem. Runtime Assurance for Safe and Fair Sequential Decision Making. | EATCS Award. (Chair: Pawel Sobocinski) Samson Abramsky. The quest for structure. |
| Abstract. Bounded arithmetic is a
collection of first-order theories that serves as a framework for studying
problems in definability, probability, and complexity. It brings
together topics in provably total functions and TFNP functions, propositional
proof complexity, and independence results. This talk will survey
results in this area, both old and new. |
Abstract. In this talk, we will explore methods to enforce formally specified safety and fairness properties during runtime. The main focus will be on shielded reinforcement learning. Shields use a model of the environment’s behaviour to analyse the safety of actions and prevent the learning agent from executing any action that could potentially violate a formal safety specification. In the talk, we will discuss how shields can be computed for environments that inherit both probabilistic and adversarial behaviour. Additionally, we will examine recent advancements in shielding, including shields that are robust under delayed input observation and shielding under partial observability. We will also discuss recent automata learning approaches capable of deriving compact probabilistic models for high-dimensional environments, which can be used to compute shields. In the second part of the talk, we will discuss how similar methods can be used to enforce fairness properties during runtime while minimizing the costs associated with interfering with the learned decision-maker. | Abstract. I have worked on a number of topics in the logic and semantics of computation, including domain theory and duality, game semantics, categorical quantum mechanics, contextuality in quantum mechanics and beyond, and game comonads as a foundation for resource-sensitive model theory. I will discuss a few key ideas and results, and identify some underlying themes. | |
| 17:15 | Church Award. (Chair: Anuj Dawar) Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus: from semantics to syntax | ||
| Abstract. Linear logic, introduced by Girard in 1986, is a logical Curry-Howard account of linear algebra. It deeply relates the algebraic notion of linearity with computational linearity: a program is linear if it uses completely and exactly once its input. Linear logic also admits exponential modalities that allow to host non-linear proofs/morphisms corresponding roughly speaking to lambda-terms in the syntax and to analytic functions in the semantics. We will show how, in some models of linear logic, dereliction - the rule that embeds linear functions into analytic ones - has a kind of inverse that should be understood as extracting from a non-linear morphism its "best linear approximant", that is as differentiation. From this observation we derive a differential extension of linear logic which takes the form of new rules for the exponentials, symmetric to the usual ones. We will describe the corresponding extension of the lambda-calculus, the differential lambda-calculus, featuring a syntactic operation of differentiation based on the usual laws of the differential calculus. We will present the Taylor expansion of lambda-terms which is based on an iterated use of these syntactic derivatives and provides a fine grain algebraic theory of finite approximations of programs, deeply connected with intersection types disciplines and game semantics. If time permits, we will discuss the analogies and differences with automated differentiation. | |||
| 17:30 | |||
| 18:00 | EATCS General Assembly and ICALP business meeting. | ||
| 19:25 |
Thursday 11 July morning invited talk
| TIME | ICALP INVITED
TALK (Chair: Karl Bringmann) Auditorium Maximum - A002 |
| 09:00 | Merav Parter. Graphs Shortcuts: New Bounds and Algorithms. |
| Abstract. For an n-vertex digraph G=(V,E), a shortcut set is a (small) subset of edges H taken from the transitive closure of G that, when added to G guarantees that the diameter of G ∪ H is small. Shortcut sets, introduced by Thorup in 1993, have a
wide range of applications in algorithm design, especially in the context of
parallel, distributed and dynamic computation on directed graphs. A folklore
result in this context shows that every n-vertex digraph admits a shortcut set of linear size (i.e., of
O(n) edges) that reduces the diameter to Õ(√n). Despite extensive research over the years, the question of
whether one can reduce the diameter to o(√n) with Õ(n) shortcut edges has been left open.
In this talk, I will
present the first improved diameter-sparsity tradeoff for this problem,
breaking the √n
diameter barrier. Specifically, we show an O(nω)-time randomized algorithm for computing a linear shortcut set
that reduces the diameter of the digraph to Õ(n⅓). I also present time efficient algorithms for computing these
shortcuts and explain the limitations of the current approaches. Finally, I
will draw some connections between shortcuts and several forms of graph
sparsification (e.g., reachability preservers, spanners).
Based on a joint work with Shimon Kogan (SODA 2022, ICALP 2022, FOCS 2022, SODA 2023). |
|
| 09:55 |
Thursday 11 July morning regular session
| TIME | LICS S8 -
VECTOR ADDITION SYSTEMS AND CSP (Chair: Georg Zetzsche) Auditorium Maximum - A002 |
FSCD S3 - PROOF
THEORY AND LOGIC I (Chair: Herman Geuvers) Europe Hall - A222 |
ICALP A/B JOINT
SESSION (Chair: Steffen van Bergerem) Tallinn Hall - M218 |
ICALP A14 -
DYNAMIC GRAPH ALGORITHMS (Chair: Shiri Chechik) A543 |
ICALP A15
-GEOMETRY (Chair: Sándor Kisfaludi-Bak) A325 |
| 10:30 | Eren
Keskin and Roland Meyer. On the Separability Problem of VASS
Reachability Languages (distinguished paper) |
Pablo Donato. The Flower Calculus | Manon Blanc and Olivier Bournez. The complexity of computing in continuous time: space complexity is precision | Michal Dory, Sebastian Forster, Yasamin Nazari and Tijn de Vos. New Tradeoffs for Decremental Approximate All-Pairs Shortest Paths | Fateme Abbasi, Sandip Banerjee, Joachim Spoerhase, Ameet Gadekar, Roohani Sharma, Jaroslaw Byrka, Kamyar Khodamoradi, Parinya Chalermsook and Dániel Marx. Parameterized Approximation for Robust Clustering in Discrete Geometric Spaces |
| 10:45 | Michael Blondin, Alain Finkel, Piotr Hofman, Filip Mazowiecki and Philip Offtermatt. Soundness of reset workflow nets | ||||
| 10:55 | Yuya Uezato. Regular Expressions with Backreferences and Lookaheads Capture NLOG | Yaowei Long and Yunfan Wang. Better Decremental and Fully Dynamic Sensitivity Oracles for Subgraph Connectivity | Artur Czumaj, Guichen Gao, Shaofeng H.-C. Jiang, Robert Krauthgamer and Pavel Veselý. Fully-Scalable MPC Algorithms for Clustering in High Dimension | ||
| 11:00 | A. R. Balasubramanian. Decidability and Complexity of Decision Problems for Affine Continuous VASS | G. A. Kavvos. Two-dimensional Kripke Semantics | |||
| 11:15 | Manuel Bodirsky, Žaneta Semanišinová and Carsten Lutz. The Complexity of Resilience Problems via Valued Constraint Satisfaction Problems | ||||
| 11:20 | Aaron Potechin and Aaron Zhang. Bounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle | Aditi Dudeja. Decremental Matching in General Weighted Graphs | Pritam Acharya, Sujoy Bhore, Aaryan Gupta, Arindam Khan, Bratin Mondal and Andreas Wiese. Approximation Schemes for Geometric Knapsack for Packing Spheres and Fat Objects | ||
| 11:30 | Victor Dalmau and Jakub Opršal. Local consistency as a reduction between constraint satisfaction problems | Junyoung Jang, Sophia Roshal, Frank Pfenning and Brigitte Pientka. Adjoint Natural Deduction | |||
| 11:45 | Libor Barto, Silvia Butti, Alexandr Kazda, Caterina Viola and Stanislav Živný. Algebraic Approach to Approximation | Noel Arteche, Erfan Khaniki, Ján Pich and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols | Adam Karczmarz and Marcin Smulewicz. Fully Dynamic Strongly Connected Components in Planar Digraphs | Mónika Csikós and Nabil Mustafa. An Optimal Sparsification Lemma for Low-Crossing Matchings and its Applications | |
| 12:00 | Lorenzo Ciardo, Marcin Kozik, Andrei Krokhin, Tamio-Vesa Nakajima and Stanislav Živný. 1-in-3 vs. Not-All-Equal: Dichotomy of a broken promise | Ambrus Kaposi and Szumi Xie. Second-order generalised algebraic theories: signatures and first-order semantics | |||
| 12:10 | Rajesh Jayaram, Jakub Łącki, Slobodan Mitrović, Krzysztof Onak and Piotr Sankowski. Dynamic PageRank: Algorithms and Lower Bounds | Chiranjib Bhattacharyya, Ravindran Kannan and Amit Kumar. Random Separating Hyperplane Theorem and Learning Polytopes | |||
| 12:15 | Demian Banakh and Marcin Kozik. Injective hardness conditions for PCSPs | ||||
| 12:25 |
Thursday 11 July afternoon invited talk
| TIME | LICS/FSCD JOINT
INVITED TALK (Chair: Ugo Dal Lago) Auditorium Maximum - A002 |
| 14:00 | Martín Escardó. Topology in constructive mathematics and computer science. |
| Abstract. Topology provides a bridge between the finite nature of computers and the infinite nature of mathematical objects we want to compute with. The first part of the talk will review the history and main contributions of various protagonists, building on the pioneering insights of Brouwer, Kleene, Kreisel, Myhill & Shepherdson, Scott, Smyth, Voevodsky, among others. The second part of the talk will discuss my own work, old and recent, including the development of topological ideas in type theory, which serves both as a programming language and as a foundation of constructive mathematics. The talk will be addressed to a general audience, and will not assume familiarity with topology or type theory. | |
| 14:55 |
Thursday 11 July afternoon regular session
| TIME | LICS S9 -
AUTOMATA THEORY (Chair: Nobuko Yoshida) Auditorium Maximum - A002 |
FSCD S4 - PROOF
THEORY AND LOGIC II (Chair: Giulio Guerrieri) Europe Hall - A222 |
ICALP B4 -
CONSTRAINT SATISFACTION AND HOMOMORPHISMS (Chair: Sandra Kiefer) Tallinn Hall - M218 |
ICALP A16 -
STREAMING ALGORITHMS (Chair: Artur Czumaj) A325 |
ICALP A17 -
PARAMETERIZED ALGORITHMS III (Chair: Roohani Sharma) A543 |
| 15:30 | Emmanuel Filiot, Ismaël Jecker, Christof Löding, Anca Muscholl, Gabriele Puppis and Sarah Winter. Finite-valued Streaming String Transducers | Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti | Antoine Mottet, Tomáš Nagy and Michael Pinsker. An order out of nowhere: a new algorithm for infinite-domain CSPs | Shiri Chechik, Doron Mukhtar and Tianyi Zhang. Streaming Edge Coloring with Subquadratic Palette Size | Christophe Paul, Evangelos Protopapas, Dimitrios Thilikos and Sebastian Wiederrecht. Delineating Half-Integrality of the Erdős-Pósa Property for Minors: the Case of Surfaces |
| 15:45 | Udi Boker. Discounted-Sum Automata with Real-Valued Discount Factors | ||||
| 15:55 | Alberto Larrauri and Stanislav Živný. Solving promise equations over monoids and groups | Soheil Behnezhad and Mohammad Saneian. Streaming Edge Coloring with Asymptotically Optimal Colors | Carla Groenland, Isja Mannens, Jesper Nederlof, Marta Piecyk and Paweł Rzążewski. Towards Tight Bounds for the Graph Homomorphism Problem Parameterized by Cutwidth via Asymptotic Matrix Parameters | ||
| 16:00 | Ismaël Jecker, Filip Mazowiecki and David Purser. Determinisation and Unambiguisation of Polynomially-Ambiguous Rational Weighted Automata | Victor
Sannier and Patrick Baillot. A linear Type System for Lp-Metric Sensitivity
Analysis (best paper by junior researcher) |
|||
| 16:15 | Pierre Ohlmann and Mikołaj Bojańczyk. Rank-decreasing transductions | ||||
| 16:20 | Jakub Rydval. Homogeneity and Homogenizability: Hard Problems for the Logic SNP | Prantar Ghosh and Manuel Stoeckl. Low-Memory Algorithms for Online Edge Coloring | Marin Bougeret, Bart M. P. Jansen and Ignasi Sau. Kernelization Dichotomies for Hitting Subgraphs under Structural Parameterizations | ||
| 16:30 | Benedict Bunting and Andrzej Murawski. Contextual Equivalence for State and Control via Nested Data | René Thiemann and Akihisa Yamada. A verified algorithm for deciding pattern completeness | |||
| 16:45 | Laura Ciobanu and Georg Zetzsche. Slice closures of indexed languages and word equations with counting constraints | Jakub Rydval, Žaneta Semanišinová and Michał Wrona. Identifying Tractable Quantified Temporal Constraints within Ord-Horn | Yu Chen, Michael Kapralov, Mikhail Makarov and Davide Mazzali. On the Streaming Complexity of Expander Decomposition | Klaus Heeger, Danny Hermelin, Matthias Mnich and Dvir Shabtay. No Polynomial Kernels for Knapsack | |
| 17:00 | Ashwani Anand, Sylvain Schmitz, Lia Schütze and Georg Zetzsche. Verifying Unboundedness via Amalgamation | Andrej Dudenhefner and Daniele Pautasso. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions | |||
| 17:10 | Benjamin Scheidt. On Homomorphism Indistinguishability and Hypertree Depth | Ce Jin, Michael Kapralov, Sepideh Mahabadi and Ali Vakilian. Streaming Algorithms for Connectivity Augmentation | Somnath Bhattacharjee, Markus Bläser, Pranjal Dutta and Saswata Mukherjee. Exponential lower bounds via exponential sums | ||
| 17:15 | Arka Ghosh and Sławomir Lasota. Equivariant ideals of polynomials | ||||
| 17:25 |
Thursday 11 July LiCS poster session
18:00-19:00
Ali Asadi. Deterministic Sub-exponential Algorithm for Discounted-sum Games with Unary Weights
Lorenzo Ciardo. Quantum advantage and CSP complexity
Alessandro Di Giorgio. Diagrammatic Algebra of First Order Logic
Arka Ghosh. Equivariant ideals of polynomials
Sergey Goncharov. Higher-Order Mathematical Operational Semantics
Vincent Michielini. On the complexity of Maslov’s class K
Vincent Michielini. Uniformisation of Regular Relations in First-Order Logic with Two Variables
Yoàv Montacute. Concurrent Games over Relational Structures: The Origin of Game Comonads
Mihir Vahanwala. On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates
Tamio-Vesa Nakajima. 1-in-3 vs. Not-All-Equal: Dichotomy of a broken promise
Harry Vinall-Smeeth. From Quantifier Depth to Quantifier Number: Separating Structures with k Variables
Friday 12 July morning invited talk
| TIME | LICS/ICALP/FSCD
JOINT INVITED TALK (Chair: Thore Husfeldt) Auditorium Maximum - A002 |
| 09:00 | Edith Elkind. Group Fairness: Multiwinner Voting and Beyond. |
| Abstract. In multiwinner voting with approval ballots the agents are presented with a set of alternatives, each agent indicates which of these alternatives they approve, and the goal is to select a fixed-size subset of the alternatives, in a way that reflects the voters' preferences. This framework captures a variety of group decision-making scenarios, from choosing a list of speakers for an event to appointing a set of validators in a proof-of-stake blockchain. An important concern in many of these scenarios is group fairness: every sufficiently large group of agents with similar preferences should be represented in the winning set of alternatives. In this talk, we discuss how to formalise this idea and whether the resulting axioms can be satisfied by efficiently computable voting rules. We also discuss extensions of our framework to the more expressive setting of participatory budgeting, where the agents are presented with a slate of projects (which may have different costs) and the goal is to select a subset of projects subject to a budget constraint. | |
| 09:55 |
Friday 12 July morning regular session
| TIME | FSCD S5 -
CONSTRUCTIVE MATH AND PROGRAMMING LANGUAGES (Chair: Tarmo Uustalu) Europe Hall - A222 |
ICALP B5 -
FINITE MODELS, GRAPHS, AND COMPLEXITY (Chair: Joel Ouaknine) Tallinn Hall - M218 |
ICALP A18 -
ONLINE ALGORITHMS (Chair: Jiri Sgall) Auditorium Maximum - A002 |
ICALP A19-
APPROXIMATE COUNTING (Chair: Jacob Focke) A325 |
ICALP A20 -
DATA STRUCTURES (Chair: Seth Pettie) A543 |
| 10:30 | Hugo Herbelin and Jad Koleilat. On the logical structure of some maximality and well-foundedness principles equivalent to choice principles | Guillaume Theyssier. FO logic on cellular automata orbits equals MSO logic | Ilan Doron and Seffi Naor. Non-Linear Paging | Keren Censor-Hillel, Tomer Even and Virginia Vassilevska Williams. Fast Approximate Counting of Cycles | Kasper Green Larsen, Rasmus Pagh, Giuseppe Persiano, Toniann Pitassi, Kevin Yeo and Or Zamir. Optimal Non-Adaptive Cell Probe Dictionaries and Hashing |
| 10:55 | Michael Benedikt, Chia-Hsuan Lu, Boris Motik and Tony Tan. Decidability of Graph Neural Networks via Logical Characterizations | Yaniv Sadeh and Haim Kaplan. Caching Connections in Matchings | Holger Dell, John Lapinskas and Kitty Meeks. Nearly optimal independence oracle algorithms for edge estimation in hypergraphs | William Kuszmaul and Zoe Xi. Towards an Analysis of Quadratic Probing | |
| 11:00 | Sohei Ito and Makoto Tatsuta. Representation of Peano Arithmetic in Separation Logic | ||||
| 11:20 | Amina Doumane, Samuel Humeau and Damien Pous. A finite presentation of treewidth at most 3 graphs | Yossi Azar, Shahar Lewkowicz and Danny Vainstein. List Update with Delays or Time Windows | Weiming Feng and Heng Guo. An FPRAS for two terminal reliability in directed acyclic graphs | Parinya Chalermsook, Manoj Gupta, Wanchote Jiamjitrak, Akash Pareek and Sorrachai Yingchareonthawornchai. The Group Access Bounds for Binary Search Trees | |
| 11:30 | Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva and Fabio Zanasi. On Iteration in Discrete Probabilistic Programming | ||||
| 11:45 | Jakub Gajarský and Rose McCarty. On classes of bounded tree rank, their interpretations, and efficient sparsification | Sariel Har-Peled, Elfarouk Harb and Vasilis Livanos. Oracle-Augmented Prophet Inequalities | Konrad Anand, Weiming Feng, Graham Freifeld, Heng Guo and Jiaheng Wang. Approximate counting for spin systems in sub-quadratic time | Djamal Belazzougui, Gregory Kucherov and Stefan Walzer. Robust Set Reconciliation | |
| 12:00 | Kostia Chardonnet, Louis Lemonnier and Benoît Valiron. Semantics for a Turing-complete Reversible Programming Language with Inductive Types | ||||
| 12:10 | Christoph Haase, Shankara Naryananan Krishna, Khushraj Madnani, Om Swostik Mishra and Georg Zetzsche. An efficient quantifier elimination procedure for Presburger arithmetic | Shaofeng H.-C. Jiang, Wenqian Wang, Yubo Zhang and Yuhao Zhang. Algorithms for the Generalized Poset Sorting Problem | Charlie Carlson, Ewan Davies, Alexandra Kolla and Aditya Potukuchi. A spectral approach to approximately counting independent sets in dense bipartite graphs | Kento Iseri, Tomohiro I, Diptarama Hendrian, Dominik Köppl, Ryo Yoshinaka and Ayumi Shinohara. Breaking a Barrier in Constructing Compact Indexes for Parameterized Pattern Matching | |
| 12:25 |
Friday 12 July afternoon invited talk
| TIME | FSCD INVITED
TALK (Chair: Patrick Baillot) Europe Hall - A222 |
| 14:00 | Delia Kesner. Capturing Properties of Call-by-Name and Call-by-Value in a Subsuming Framework. |
| Abstract. This talk explores how the well-established models of
computation given by Call-by-Name (CBN) and Call-by-Value (CBV) can be
encoded within a broader setting provided by a unifying framework called the
dBang calculus. We first introduce the dBang calculus, which subsumes (untyped and typed) CBN and CBV, both from a static and a dynamic perspective. We then explore various properties of these computational models, including type inhabitation, upper bounds and exact measures for evaluation lengths, meaningfulness, and genericity. In all these cases, explained and discussed in the talk, the properties of CBN and CBV are subsumed/inherited from the corresponding counterparts within the dBang calculus. |
|
| 14:55 |
Friday 12 July afternoon regular session
| TIME | FSCD S6 -
COMBINATORICS (Chair: Jürgen Giesl) Europe Hall - A222 |
ICALP B6 -
GAMES AND VECTOR ADDITION SYSTEMS (Chair: Mikołaj Bojańczyk) Tallinn Hall - M218 |
ICALP A21 -
QUANTUM COMPUTING (Chair: Karl Bringmann) Auditorium Maximum - A002 |
ICALP A22 -
GAME THEORY (Chair: Nick Fischer) A325 |
ICALP A23 -
APPROXIMATION ALGORITHMS II (Chair: Sujoy Bhore) A543 |
| 15:30 | Samson Abramsky, Serban Cercelescu and Carmen Maria Constantin. Commutation groups and state-independent contextuality | Mohan
Sai Teja Dantam and Richard Mayr. Finite-memory Strategies for Almost-sure
Energy-MeanPayoff Objectives in MDPs |
Maxime Cautrès, Nathan Claudet, Mehdi Mhalla, Simon Perdrix, Valentin Savin and Stéphan Thomassé. Vertex-minor universal graphs for generating entangled quantum subsystems | Matan Gilboa. A Characterization of Complexity in Public Goods Games | Soheil Behnezhad, Mohammad Roghani, Aviad Rubinstein and Amin Saberi. Sublinear Algorithms for TSP via Path Covers |
| 15:55 | Bruno Loff and Mateusz Skomra. Smoothed analysis of deterministic discounted and mean-payoff games | Eunou Lee and Ojas Parekh. An improved Quantum Max Cut approximation via Maximum Matching | Soh Kumabe and Yuichi Yoshida. Lipschitz Continuous Allocations for Optimization Games | Leonid Gurvits, Nathan Klein and Jonathan Leake. From Trees to Polynomials and Back Again: New Capacity Bounds with Applications to TSP | |
| 16:00 | Mateus De Oliveira Oliveira and Farhad Vadiee. State Canonization and Early Pruning in Width-Based Automated Theorem Proving | ||||
| 16:20 | Rohan Acharya, Marcin Jurdziński and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata | Jan Olkowski, Dariusz Kowalski and Mohammad Hajiaghayi. Distributed fast crash-tolerant consensus with nearly-linear quantum communication | Junjie Chen, Minming Li, Haifeng Xu and Song Zuo. Bayesian Calibrated Click-Through Auctions | Sophia Heimann, Hung P. Hoang and Stefan Hougardy. The k-Opt algorithm for the Traveling Salesman Problem has exponential running time for k≥5 | |
| 16:30 | FSCD general meeting | ||||
| 16:45 | Yuxi Fu, Qizhe Yang and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS | Srnivasan Arunachalam, Arkopal Dutt, Francisco Escudero Gutiérrez and Carlos Palazuelos. Learning low-degree quantum objects | Yasushi Kawase, Koichi Nishimura and Hanna Sumita. Minimizing Symmetric Convex Functions over Hybrid of Continuous and Discrete Convex Sets | Yury Makarychev, Max Ovsiankin and Erasmo Tani. Approximation Algorithms for lp-Shortest Path and lp-Group Steiner Tree | |
| 17:10 | Pascal Baumann, Eren Keskin, Roland Meyer and Georg Zetzsche. Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities | Serge Gaspers and Jerry Zirui Li. Quantum Algorithms for Graph Coloring and other Partitioning, Covering, and Packing Problems | Chung Shue Chen, Peter Keevash, Sean Kennedy, Élie de Panafieu and Adrian Vetta. Robot positioning using torus packing for multisets | Shi Li, Chenyang Xu and Ruilong Zhang. Polylogarithmic Approximations for Robust s-t Path | |
| 17:25 |
Saturday 13 July morning invited talk
| TIME | FSCD INVITED
TALK (Chair: Claudio Sacerdoti Coen) Europe Hall - A222 |
| 09:00 | Sebastian Ullrich. Lean: Past, Present, and Future. |
| Abstract. The Lean programming language and theorem prover project is celebrating its tenth birthday this year, having been started by Leonardo de Moura at Microsoft Research and first released as Lean 0.1 in 2014. In this invited talk, I will review Lean’s history and unique features and discuss our roadmap for its bright future. | |
| 09:55 |
Saturday 13 July morning regular session
| TIME | FSCD S7 -
REDUCTION STRATEGIES (Chair: Naoki Nishida) Europe Hall - A222 |
| 10:30 | Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-by-Need, or Values Acting Silly |
| 11:00 | Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead |
| 11:30 | Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments |
| 12:00 | Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All! |
| 12:25 |
Saturday 13 July afternoon regular session
| TIME | FSCD S8 - TERM
REWRITING (Chair: Delia Kesner) Europe Hall - A222 |
| 14:00 | Salvador Lucas. Termination of Generalized Term Rewriting Systems |
| 14:30 | Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems |
| 15:00 | Teppei Saito and Nao Hirokawa. Simulating Dependency Pairs by Semantic Labeling |
| 15:30 | Takahito Aoto, Naoki Nishida and Jonas Schöpf. Equational Theories and Validity for Logically Constrained Term Rewriting |
| 15:55 |
Local Information
For questions regarding local organisation and local information, please email [email protected].
Venue, Tallinn and Estonia
The conferences and workshops will be held in the Astra building on the campus of Tallinn University.
The address is Narva mnt 29. This is a central location, within walking distance of the old town, and is easily accessible from the airport. There will be some disruption of local transport in Tallinn in the summer due to planned road upgrades. You can plan your trip here.
Conference participants may take the opporunity to extend their stay and visit Estonia. Estonia is truly magical in early July – there's plenty of sun and the evenings are long and warm. The portal visit estonia is a great source of tourist information.
For useful advice and inspiration on Tallinn’s top attractions, activities, events, and places to eat and drink, check out the city’s official tourism portal, visittallinn.ee, or follow @VisitTallinn on social media
.
July 9 Welcome Reception
Venue: Kadriorg Art Museum (housed in the Kadriorg Palace)
Address: Weizenbergi 37
Walk from the Conference Venue : 1,1 km / 16 minutes
July 10 Joint Banquet
Venue: Seaplane Harbour Museum
Address: Vesilennuki 6
Distance from the Conference Venue ca 3 km. Transfers will be provided from the conference venue.
Accommodation
There are plenty of accommodation choices for all budgets in the area. We have an agreed discount rate for a limited number of rooms for conference participants at several local hotels:
Nordic Hotel Forum, (4* superior), Viru väljak 3, which is 15 minutes walk or a 3 minute tram ride from the conference location. Nordic Hotel Forum is a 4 star superior hotel in the prime location in Tallinn that has recently completed a full renovation to the entire hotel. The hotel offers spacious and elegant hotel rooms and a Leisure Centre on the 8th floor with magnificent views over the historic Old Town of Tallinn. The price includes buffet breakfast, free WiFi and use of hotel’s leisure centre on the top floor with fully equipped gym, indoor pool and saunas. Book here.
Kalev Spa Hotel and Water Park, (4*), Aia St 18, 20 minutes walk from the conference venue and accessible by Bus Line 8, stop Ahtri to Uus-Sadama. Located near the historic Old Town and the culturally vibrant seashore area. Perfect for both leisure and business travellers looking to rejuvenate body and soul with the ultimate spa experience. Modern amenities, including luxurious spa facilities, indoor pools, and comfortable accommodation. Book here.
Radisson Park Inn Central, (3*), Narva Rd 7c, 10 minutes walk from conference venue or easily accesssible via tram. Located a 5-minute walk away from the medieval old town. The price includes breakfast and free Wi-Fi. Well accessible from the Airport and Port of Tallinn. Book here.
Go Hotel Schnelli, (3*), Toompuiestee 37/1, 35 minutes walk to the conference venue or accessible in ~20 mins by public transport via Bus number 8, Stop Balti Jaam to Uus-Sadama. A budget-friendly hotel, located in the immediate vicinity of Tallinn's Old Town and the historic railway passenger terminal, Balti Jaam. Right next to the vibrant Kalamaja district and the Telliskivi area, known for its numerous popular restaurants and venues. A perfect location for evening hang-outs! Book here.
Hestia Hotel Barons, (4*), Suur-Karja 7, located in the Old Town, 25 minutes walk or a short tram ride to the conference venue. Book here.
Hestia Hotel Europa, (4*), Paadi St 5, 13 minute walk from the conference venue. Book here.
Hestia Hotel Seaport, (3*), Uus-Sadama St 23, 9 minute walk from the conference venue. Book here.
Getting there and local transport
Tallinn Airport offers direct flights to many European cities and is also well-connected to several regional hubs, with several daily flights to Helsiki, Warsaw, Stockholm and Frankfurt.
It is also possible to get to Tallinn by ferry from Helsiki (~2 hours, several daily connections), and by coach from Riga, Vilnius and other cities in the Baltic region.
While Tallinn has an excellent and affordable local transport network, please note that there are major road construction works going on in the Tallinn City centre, as a new tram line is being built. Check the routes/stops situation, how to get to your needed locations. There is relevant/current data available on the Tallinn website.
The conference is supported by the City of Tallinn. All the participants will get a free Tallinn public transportation pass. Relevant details will be sent in due course.
Some links you might find useful planning your trip:
Ministry of Foreign Affairs (visa and consular issues, crossing the border, …) https://vm.ee/en
Visit Estonia (the official travel guide to Estonia) https://www.visitestonia.com/en/
Visit Tallinn (plan your trip, getting to the centre, see&do, …) https://www.visittallinn.ee/eng/visitor
Tallinn Airport https://airport.ee/en/tallinn-airport/
Port of Tallinn https://www.ts.ee/en/departures/
Tallinn Coach Station https://www.bussijaam.ee/en/tickets/
Public transportation routes and timetables_Tallinn https://transport.tallinn.ee/#tallinna-linn/en
Reconstruction of the roads in Tallinn https://www.tallinn.ee/en/vanasadamatramm