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:
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
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
Organizing and Program Committee
Below you can find the exhaustive list of previous CLA editions:
