17th Workshop

14-15 December 2023

It is our pleasure to announce that the 17th workshop on
*Computational Logic and Applications* will be held in December 2023,
as a hybrid workshop at the Jagiellonian University in Kraków and online.

This edition is organised on the occasion of the 70th birthday of Marek Zaionc. Marek is a professor at the Jagiellonian University and a co-founder of CLA workshops. As an accompanying event, a birthday scientific session will be held on Wednesday, 13 December 2023.

The main purpose of CLA is to provide an open, free access forum for scientific research concentrated around combinatorial and quantitative aspects of mathematical logic and their applications in computer science.

We cordially invite all researchers interested in topics such as:

- combinatorics of lambda calculus, sequent calculi, and related logical formalisms, as well as their interactions with the combinatorics of maps and related objects;
- combinatorics of lattices derived from logic or rewriting;
- asymptotic enumeration and statistical properties of formulae, types, proofs, programs, etc.;
- quantitative aspects of program evaluation and normalisation;
- random generation with applications to logic and programming;
- randomness in software testing and counter-example generation.

Wojciech Czerwiński (University of Warsaw)

*The Reachability Problem for Computation Models *

- Cameron Calk and Luigi Santocanale

*Lattices of Paths and Flat Dihomotopy Types* - Peter Hines

*“It’s all Greek to me”– on the pre-history of coherence in categorical logic* - Jean-Michel Hufflen

*Implementing Escape Continuations in C* - Jakub Kozik

*One more proof of Thue's theorem on nonrepetitive sequences* - Mehdi Naima

*A lattice on Dyck paths close to the Tamari Lattice* - Ryoma Sin'ya

*Asymptotic Approximation in Formal Languages* - Noam Zeilberger

*The combinatorics of free bifibrations*

The aim of this session is not only to encourage participants to present the problems they are currently struggling with, but also to provide an opportunity for collaborative brainstorming. Everyone interested in sharing an open problem is asked to send a notice to grygiel@tcs.uj.edu.pl

All the times below are given in **Warsaw Time (UTC+1)**.

9:40-10:00 **Welcome coffee**

10:00-11:00 **Wojciech Czerwiński**

*( Invited talk) The Reachability Problem for Computation Models*

The reachability problem is arguably one of the most fundamental problems for computation models. Since the 1950-ties we know that the halting problem is undecidable for Turing machines, which is exactly the reachability problem for Turing machines.

What happens for other natural computation models, which can be composed from pushdowns, zero-test counters, non-zero-tested counters etc.? I will show that despite of decades of intense research with many successes there are still a lot of stunning question marks in this area. I plan to illustrate it with simple examples for a few natural systems, which will convince you that they often become surprisingly involved.

11:00-11:30 **Coffee break**

11:30-12:00 **Jean-Michel Hufflen**

*Implementing Escape Continuations in C*

This work is contributing to implementing escape continuations by means of the C functions "setjmp" and "longjmp". We define a semantics for the statements of the C language by means of continuations. That allows us to express jump statements such that break or continue. Then the statements "setjmp" and "longjmp" are given precise semantics.

These statements "setjmp" and "longjmp" can be used to implement *escape continuations*. By *escape continuations*, we mean continuations captured by the Scheme function "call/cc", except that these continuations only have dynamic extend, that is, they cannot be used as snapshots, saved and played again. We can consider that they belong to the "control_cont" type of Standard ML of New Jersey.

It is well known that escape continuations are used to escape successive recursive calls leading to a dead-end calculation. We show that an equivalent implementation using "setjmp" and "longjmp" is correct, that is:

let "f" be such a function--using escape continuations--written in Scheme or
Standard ML of New Jersey, let "x" (resp. "y") be an element

of "f"'s domain
(resp. codomain); if we denote the respective implementations in C by C(f),
C(x), C(y), then:

f(x) = y ===> C(f)(C(x)) = C(y)

The interest of this work is related to compiling languages such as Scheme or Standard ML of New Jersey by generating C code, a C compiler being in charge of low-level details. Besides, it is a complement of articles describing the implementation of exceptions by means of the C functions "setjmp" and "longjmp". An implementation using Coq is in progress.

**Slides**
**tree-sum-ep.scp**
**tree-sum-ep.sml**

12:15-13:15 **Lunch break**

13:15-13:45 **Ryoma Sin'ya**

*Asymptotic Approximation in Formal Languages*

13:50-14:20 **Jakub Kozik**

*One more proof of Thue's theorem on nonrepetitive sequences*

Pattern avoidance is a deeply studied problem within the field of combinatorics onwords. One of the seminal results of this area is the theorem of Thue which asserts that there exists an infinite word over three letter alphabet, in which no two consecutive substrings are identical. A number of proofs of this fact are known. Few are as simple as the original one. Most of them, however, illustrate techniques which can applied in other contexts.

A variant of the problem, that we are interested in, is called the *choosability version*.
In that case the alphabet is not fixed but for every position of the sequence the choice of symbols
is (independently) constrained. If for each position we can chose a letter from a set of size at least
four, then it is always possible to construct an arbitratily long nonrepetitive sequence. It is not known
to be true when there are only three options (or even three in every second step and four in every other).
First result of this kind was obtained by Alon, Grytczuk, Hałuszczak and Riordan in 2001 by an application
of Lovasz Local Lemma. All consecutive improvements (on the sufficient number of options) was obtained by
more refined applications and more specific variants of the lemma. In a sense, for some time, this problem
served as a benchmark for probabilistic local techniques.

We are going to discuss another proof of Thue’s theorem, which is the result of combining so called
*entropy compression argument* with approximation of the language of nonrepetitive words by regular
languages. It is our hope that this line of reasoning can be generalised in a way that would allow to
improve the results on the choosability version of the problem.

14:25-14:55 **Mehdi Naima**

*A lattice on Dyck paths close to the Tamari Lattice*

15:00-15:30 **Coffee break**

15:30-? **Open problem session**

10:10-10:40 **Noam Zeilberger**

*The combinatorics of free bifibrations*

10:45-11:15 **Cameron Calk and Luigi Santocanale**

*Lattices of Paths and Flat Dihomotopy Types*

11:20-11:50 **Peter Hines**

*“It’s all Greek to me”– on the pre-history of coherence in categorical logic*

12:00 **Lunch**

Registration is **open**!

Click here to register your intention to participate. Whether in person or online, attendance is free. Please remember, however, to meet the registration deadlines.

Talk proposals should consist of short abstracts of up to three pages, and may describe either ongoing or previously published work. Submissions should be sent by email to the organizers (see below).

Depending on the number of submissions, contributed talks will be 20-30 minutes long.

: submission deadline for talk proposals~~November 7~~November 14, 2023 (AoE): speaker notification~~November 15~~November 18, 2023 (AoE)*November 20, 2023*: registration deadline for in-person attendance*December 10, 2023*: registration deadline for online attendance*December 13, 2023*: birthday session*December 14-15, 2023*: workshop

The workshop will be held at the
Faculty of Mathematics and Computer Science at the Jagiellonian University (ul. Łojasiewicza 6, Kraków). All the talks will take place at the ground floor in ** room 0174**.

The participants are expected to book their accommodation individually.

On Thursday at 5:30 pm we meet in the restaurant **Jinling Dumpling**. It is located close to the city center. Address: Józefa Dietla 39, Kraków.

Steering Committee

- Olivier Bodini (Université Paris-Nord, Villetaneuse, France)
- Alain Giorgetti (Institut FEMTO-ST, University of Bourgogne Franche-Comté, Besançon, France)
- Bernhard Gittenberger (TU Wien, Austria)
- Katarzyna Grygiel (Jagiellonian University, Kraków, Poland)
- Ryoma Sin'ya (Akita University, Japan)
- Noam Zeilberger (Ecole Polytechnique, Paris, France)

Organizing and Program Committee

- Maciej Bendkowski, in person
- Olivier Bodini (Université Sorbonne Paris Nord), online
- Cameron Calk (Laboratoire d'Informatique et Systèmes, Aix-Marseille Université), in person
- Wojciech Czerwiński (University of Warsaw), in person
- Wenjie Fang (LIGM, Université Gustave Eiffel), online
- Samuele Giraudo (LACIM, Université du Québec à Montréal), online
- Bernhard Gittenberger (TU Wien), online
- Zbigniew Gołębiewski (Wroclaw University of Science and Technology), in person
- Katarzyna Grygiel (Jagiellonian University), in person
- Peter Hines (University of York), online
- Ryuya Hora (University of Tokyo), online
- Jean-Michel Hufflen (FEMTO-ST/DISC), in person
- Farzad Jafarrahmani (Sorbonne Université, LIP6), online
- Sergey Kirgizov (LIB, Université de Bourgogne, Dijon, France), online
- Zofia Kostrzycka (Opole University of Technology), in person
- Jakub Kozik (Jagiellonian University), in person
- Vincent Moreau (IRIF, Université Paris Cité, Inria Paris), online
- Mehdi Naima (Sorbonne Université), online
- Fatih Ozkaynak (Firat University), in person
- Luigi Santocanale (LIS/AMU), online
- Michał Sochański, online
- Alexandros Singh (LIASD, Paris 8), online
- Ryoma Sin'ya (Akita University), in person
- Rick Statman (Carnegie Mellon University), online
- Tadaaki Tanimoto, online
- Bartosz Walczak (Jagiellonian University), in person
- Michael Wallner (TU Wien), online
- Marek Zaionc (Jagiellonian University), in person
- Noam Zeilberger (Ecole Polytechnique), in person

Below you can find the exhaustive list of previous CLA editions:

- 2023, Paris (France)
- 2020, on-line
- 2019, Versailles (France)
- 2018, Paris (France)
- 2017, Göteborg (Sweden)
- 2016, Novi Sad (Serbia)
- 2015, Lyon (France)
- 2012, Kraków (Poland)

- 2011, Wien (Austria)
- 2010, Kraków (Poland)
- 2009, Lyon (France)
- 2008, Kraków (Poland)
- 2007, Kraków (Poland)
- 2005, Chambery (France)
- 2004, Lyon (France)
- 2002, Kraków (Poland)