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

  Thursday, January 12th

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

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

Slides      Video

17:00-17:45  Business meeting

  Friday, January 13th

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.

Paper (external)     Slides      Video


Registration is now closed!

Important dates

  • November 30, 2022 (AoE): submission deadline for talk proposals
  • December 7, 2022 (AoE): speaker notification
  • December 16, 2022 January 1, 2023: registration deadline for in-person attendance
  • January 9, 2023: registration deadline for online attendance
  • January 12-13, 2023: workshop

Local information

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

Organizing and Program Committee

List of participants

  1. Olivier Bodini (Université Sorbonne Paris Nord), in person
  2. Nigel Burke, online
  3. Aggeliki Chalki (Reykjavik University), online
  4. Cédric de Lacroix (Aix-Marseille Université), in person
  5. Catherine Dubois (ENSIIE), in person
  6. Aloÿs Dufour (LIPN), in person
  7. Uli Fahrenberg (LRE, EPITA), in person
  8. Wenjie Fang (LIGM, Université Gustave Eiffel), in person
  9. Peter Faul (LIX), in person
  10. Michal Jan Gajda (Migamake Pte Ltd), online
  11. Zeinab Galal (University of Manchester), in person
  12. Antoine Genitrini (Sorbonne Université -- LIP6), in person
  13. Alain Giorgetti (Institut FEMTO-ST), in person
  14. Samuele Giraudo (LaCIM, UQAM), online
  15. Bernhard Gittenberger (TU Wien), in person
  16. Björn Gohla, online
  17. Katarzyna Grygiel (Jagiellonian University), online
  18. Stefano Guerrini (LIPN, Université Sorbonne Paris Nord), online
  19. Peter Hines (University of York), in person
  20. Farzad Jafarrahmani (Université Paris Cité, IRIF), in person
  21. Wolfram Kahl (McMaster University), online
  22. Pierre Lescanne (LIP, ENS LYON, University of Lyon, ), in person
  23. Nicolas Magaud (ICUBE - UMR 7357 CNRS Université de Strasbourg ), in person
  24. Orestis Melkonian (University of Edinburgh), online
  25. Dale Miller (Inria Saclay), in person
  26. Le Thanh Dung NGUYEN (ENS Lyon), in person
  27. David Nowak (CNRS), online
  28. Maria Osório (University of Lisbon), online
  29. Martin Pépin (LIPN), in person
  30. Maciej Piróg (Standard Chartered), in person
  31. John Power (Macquarie University), online
  32. Alexandros Singh (LIPN, Université Sorbonne Paris Nord), online
  33. Maximos Skandalis, online
  34. Richard Statman (Carnegie Mellon University), online
  35. Lutz Straßburger (Inria), in person
  36. Dorine Tabary (UFR-ST), online
  37. Tadaaki Tanimoto (Sony Semicondutor Solutions Corporation), online
  38. Riccardo Treglia (Unviersità di Bologna), online
  39. Tarmo Uustalu (Reykjavik University), online
  40. Michael Wallner (TU Wien), online
  41. Marek Zaionc (Jagiellonian University), online
  42. Noam Zeilberger (Ecole Polytechnique), in person


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