16th Workshop

12-13 January 2023

It is our pleasure to announce that the 16th workshop on
*Computational Logic and Applications* will be held in January 2023,
as a hybrid workshop at Ecole Polytechnique (south of Paris) and online.

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.

**Be careful:** All the times below are given in **Paris Time (UTC+1)**.

Note that all talks on Thursday will take place in **Salle Gilles Kahn** on the ground floor of LIX, and will be simultaneously streamed online.

13:15-13:30 **Welcome**

13:30-14:05 **Pierre Lescanne**

*Holonomic equations and efficient random generation of binary trees*

**Extended abstract
Slides
Video**

14:05-14:40 **Wenjie Fang**

*Bijections between planar maps and planar linear normal λ-terms with connectivity condition.*

**Extended abstract
Slides
Video**

14:40-15:15 Catherine Dubois and Alain Giorgetti and **Nicolas Magaud**

*Closable and uniquely closable skeletons of untyped lambda terms, formally*

**Extended abstract
Slides
Video**

15:15-15:45 **Coffee Break**

~~15:45-16:45~~ 16:00-17:00 **Richard Statman** (online)

*Cayley Monoids and Linear Lambda Calculus*

In 1937 Church formulated lambda calculus as a semigroup; more precisely, with eta conversion, as a monoid. Conversely, it is natural to ask when a monoid can support an application operation. Indeed, in 1975 Dana Scott said that we should view combinatory logic as "combinatory algebra"; so, let us try this. In this note we propose a possible modus operandi; namely, the notion of a Cayley monoid. Everyone is familiar with Cayley's regular representation of groups in the symmetric group. It is clear that it applies in a limited way to monoids. The notion of a Cayley monoid is just an internalization of this type of representation.

Definition: A Cayley monoid $K$ is a structure $(M,*,i,a,b,A,B)$ where

- $(M,*,i)$ is a monoid
- $a,b : M$
- $A : M \to M$ and $B : M \to M$ such that for all $x,y,z:M$
- $A(a * B(x)) = A(x)$
- $A(b * B(x)) = B(x)$
- $A(i * B(x)) = x$
- $A(x * y * B(z)) = A(x * B(A(y * B(z)))$

17:00-17:45 **Business meeting**

Note that all talks on Friday will take place in **Ampitheatre Sophie Germain** on the ground floor of LIX, and will be simultaneously streamed online.

9:30-10:05 **Alexandros Singh** (online)

*Normalisation of closed linear $\lambda$-terms and patterns in trivalent maps *

Given a large random closed linear term, what is the mean number of $\beta$-reduction steps required to bring it to its normal form? Such a question naturally arises in the study of normalisation for the untyped linear lambda calculus. By systematically enumerating special families of subterms (and patterns in trivalent maps correspondingly), we obtain an asymptotic lower bound of $\frac{12n}{240}$ steps, getting quite close to the $\frac{n}{21}$ value conjectured by Noam Zeilberger for said mean, as presented during CLA 2020.

During our investigations we observed a number of unusual behaviours for patterns in such terms maps, which we also present as motivation for further investigations into this subject.

This talk is based on joint work with Olivier Bodini, Bernhard Gittenberger, Michael Wallner, and Noam Zeilberger.

**
Slides
Video**

10:05-10:35 **Coffee Break**

10:35-11:10 Dylan McDermott and ** Maciej Piróg** and Tarmo Uustalu

*Counting Monads on Lists*

**Extended abstract
Slides
Video**

11:10-11:45 Julien Clément and **Antoine Genitrini**

*Unranking of Reduced Ordered Binary Decision Diagrams*

**Extended abstract
Slides
Video**

11:45-12:20 **Nguyễn Lê Thành Dũng**

*Simply typed β-convertibility is TOWER-complete even for safe λ-terms*

We show that deciding whether two terms of Blum and Ong's safe λ-calculus are β-convertible is TOWER-complete, just like for the simply typed λ-calculus (of which the safe λ-calculus is a fragment). This implies that it is non-elementary; previously, the best known lower bound was PSPACE. Our proof proceeds by reduction from the star-free expression emptiness problem, taking inspiration from the author's work with Pradic on "implicit automata in typed λ-calculi".

**Extended abstract
Slides
Video**

12:20-13:50 **Lunch Break**

13:50-14:25 **Peter Hines**

*Congruential Functions in Category Theory & Logic*

**Extended abstract
Slides
Video**

14:25-15:00 **Pierre Lescanne**

* Almost all classical theorems are intuitionistic*

**Extended abstract
Slides
Video**

15:00-15:35 **Michał J Gajda** (online)

*Consistent ultrafinitist logic*

Ultrafinitist logic uses computational complexity to resolve issue of total functions that are computable within resource constraints. The strict use of these constraints leads us to logic that is incomparable with Goedel's system T, and at the same time has power equivalent to Bounded Turing Machine.

This gives us a "logic of computability", that is the logic that can strictly express computable mathematics, but nothing more. It is also decidable, and thus permits a formulation of arithmetic that is both Turing-complete, and decidable. This suggests that Goedel's incompleteness theorem have much narrower scope than previously thought, since they only talk about logics with infinitary statements "hidden in plain sight", which does not apply to logics with strict bounds, even if they are Turing-complete.

**
Paper (external)
Slides
Video**

15:35-16:05 **Coffee Break**

16:05-16:40 **Samuele Giraudo** (online)

*The Mockingbird lattice*

The fragment of combinatory logic generated by the combinator M, also known as the Mockingbird, has some rich combinatorial properties. Among others, the connected components of the rewrite graph of the terms on M are Hasse diagram of lattices. Here we shall present this result by realizing this rewrite graph in terms of duplicative forests, which are some treelike structures. We also present some enumerative results about these lattices as their numbers of elements and numbers of intervals.

Registration is now **closed**!

The workshop will take place on the campus of Ecole Polytechnique, at the Alan Turing building, which houses LIX, the computer science department.
Ecole Polytechnique is located in Palaiseau to the south of Paris and is easily accessible by the RER B train: either get off at Massy Palaiseau Station and take the 91-06 or 91-10 bus to the "Polytechnique Lozère" stop followed by a 10 minute walk, or get off at Lozère Station and walk up a very long flight of stairs to the same bus stop and continue walking.
For more information about how to arrive at LIX, see this page.
The address is: **1 rue Honoré d'Estienne d'Orves, 91120 Palaiseau**.
(Once you are on the IP Paris campus you should keep in mind that it is designed as a continually evolving obstacle course of new construction sites. If you get lost, you can try jumping onto this path from the "Polytechnique Lozère" bus stop to LIX, which was navigable on 9 January.)

If you are coming to the workshop from outside of Paris and would like some advice on finding accommodations, feel free to email the workshop organisers. In addition to the many options for accommodations in Paris, there are a number of hotels in Palaiseau and Massy.

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

- Olivier Bodini (Université Sorbonne Paris Nord), in person
- Nigel Burke, online
- Aggeliki Chalki (Reykjavik University), online
- Cédric de Lacroix (Aix-Marseille Université), in person
- Catherine Dubois (ENSIIE), in person
- Aloÿs Dufour (LIPN), in person
- Uli Fahrenberg (LRE, EPITA), in person
- Wenjie Fang (LIGM, Université Gustave Eiffel), in person
- Peter Faul (LIX), in person
- Michal Jan Gajda (Migamake Pte Ltd), online
- Zeinab Galal (University of Manchester), in person
- Antoine Genitrini (Sorbonne Université -- LIP6), in person
- Alain Giorgetti (Institut FEMTO-ST), in person
- Samuele Giraudo (LaCIM, UQAM), online
- Bernhard Gittenberger (TU Wien), in person
- Björn Gohla, online
- Katarzyna Grygiel (Jagiellonian University), online
- Stefano Guerrini (LIPN, Université Sorbonne Paris Nord), online
- Peter Hines (University of York), in person
- Farzad Jafarrahmani (Université Paris Cité, IRIF), in person
- Wolfram Kahl (McMaster University), online
- Pierre Lescanne (LIP, ENS LYON, University of Lyon, ), in person
- Nicolas Magaud (ICUBE - UMR 7357 CNRS Université de Strasbourg ), in person
- Orestis Melkonian (University of Edinburgh), online
- Dale Miller (Inria Saclay), in person
- Le Thanh Dung NGUYEN (ENS Lyon), in person
- David Nowak (CNRS), online
- Maria Osório (University of Lisbon), online
- Martin Pépin (LIPN), in person
- Maciej Piróg (Standard Chartered), in person
- John Power (Macquarie University), online
- Alexandros Singh (LIPN, Université Sorbonne Paris Nord), online
- Maximos Skandalis, online
- Richard Statman (Carnegie Mellon University), online
- Lutz Straßburger (Inria), in person
- Dorine Tabary (UFR-ST), online
- Tadaaki Tanimoto (Sony Semicondutor Solutions Corporation), online
- Riccardo Treglia (Unviersità di Bologna), online
- Tarmo Uustalu (Reykjavik University), online
- Michael Wallner (TU Wien), online
- Marek Zaionc (Jagiellonian University), online
- Noam Zeilberger (Ecole Polytechnique), in person

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

- 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)