11th Workshop

Paris, France, 24-25 May 2018

It is our pleasure to announce that the eleventh workshop Computational Logic and Applications (CLA 2018) will be held on 24-25 May 2018 in Paris, France. The workshop gathers researchers interested in quantitative aspects of mathematical logic and programming, including, but not limited, to topics such as:

- combinatorics of lambda calculus and related formalisms,
- quantitative aspects of program evaluation and normalization,
- asymptotic enumeration and analytic methods in computational logic,
- enumeration and random generation of formulae, terms and programs,
- asymptotic analysis and random sampling of concurrency processes and beyond,
- random software testing and counterexample generation including Monte Carlo techniques.

All researchers are cordially invited to attend.

Program committee

- Maciej Bendkowski (Jagiellonian University, Kraków, Poland)
- Olivier Bodini (Paris-Nord University, France)
- Danièle Gardy (Versailles University, France)
- Antoine Genitrini (Sorbonne University, Paris, France)
- Alain Giorgetti (Franche-Comté University, Besançon, France)
- Bernhard Gittenberger (TU Wien, Austria)
- Zbigniew Gołębiewski (Wrocław University, Poland)
- Katarzyna Grygiel (Jagiellonian University, Kraków, Poland)
- Pierre Lescanne (École normale supérieure de Lyon, France)
- Michał Pałka (Chalmers University of Technology, Gothenburg, Sweden)
- Paul Tarau (University of North Texas, USA)
- Brent Yorgey (Hendrix College, Arkansas, USA)
- Marek Zaionc (Jagiellonian University, Kraków, Poland)
- Noam Zeilberger (University of Birmingham, United Kingdom)

- Submission of talk proposals:
*3 May 2018* - Notification of acceptance:
*5 May 2018* - Registration deadline:
*17 May 2018*

9:30-10:00 **Breakfast**

10:00-11:00 **Michael Wallner**

*Asymptotic Enumeration of Compacted Binary Trees with Height
Restrictions* (slides)

When storing rooted trees it is useful to consider compression techniques. A simple idea is to store isomorphic subtrees only once and mark repeated occurrences with a pointer. A classical algorithm to establish such a compaction was analyzed by Flajolet, Sipala, and Steyaert. The resulting structure is called a compacted tree, being in fact no more a tree but a directed acyclic graph.

Our goal is the enumeration of such structures. Since the enumeration turns out to be extremely difficult, we restrict it to a sub problem by imposing a bound on the so-called right height. We solve this enumeration problem with the help of generating functions. Due to the superexponential growth of the counting sequence we use exponential generating function despite the fact that these objects are unlabeled. We first derive a calculus on exponential generating function capturing their recursive nature. This leads to a sequence of differential equations for the generating functions (also implying their D-finiteness) for which a singularity analysis is carried out.

This work is based on joint work with Antoine Genitrini, Bernhard Gittenberger, and Manuel Kauers.

11:00-11:30 **Coffee Break**

11:30-12:30 **Antoine Genitrini**

*Compacted Binary Trees: A preliminary work on Implication
Boolean expressions represented as Directed Acyclic
Graphs* (slides)

The nature of tautologies in the context of Boolean Implication trees has been first studied by Moczurad, Tyszkiewicz and Zaionc. Their model was based on the classical Catalan tree model decorated with the connective Implication and with variables. Then several papers dealt with the same model in order to obtain quantitative results for the shape of a typical tautology. We here present the model of Compacted Binary Trees that are in fact Directed Acyclic Graphs (DAGs) and we present the first quantitative results and a recursive random generator (in fact an unranking algorithm) for this model of Boolean DAGs.

12:30-14:30 **Lunch Break**

14:30-15:30 **Isabella Larcher**

*On the number of variables in special classes of random lambda-terms
* (slides)

We investigate the number of variables in two special subclasses of lambda-terms that are restricted by a bound of the number of abstractions between a variable and its binding lambda, and by a bound of the nesting levels of abstractions, respectively. These restrictions are on the one hand very natural from a practical point of view, and on the other hand they simplify the counting problem compared to that of unrestricted lambda-terms in such a way that the common methods of analytic combinatorics are applicable. We will show that the total number of variables is asymptotically normally distributed for both subclasses of lambda-terms with mean and variance asymptotically equal to $C_1 n$ and $C_2 n$, respectively, where the constants $C_1$ and $C_2$ depend on the bound that has been imposed. So far we just derived closed formulas for the constants in case of the class of lambda-terms with a bounded number of abstractions between each variable and its binding lambda. However, for the other class of lambda-terms that we consider, namely lambda-terms with a bounded number of nesting levels of abstractions, we investigate the number of variables in the different abstraction levels and thereby exhibit very interesting results concerning the distribution of the variables within those lambda-terms.

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

15:45-16:45 **Sergey Dovgal**

*Statistical properties of lambda terms* (slides)

We consider plain and closed lambda terms sampled uniformly at random and investigate the distribution of several parameters inside them. For the number of variables, abstractions, successors and redexes we obtain normal limit laws (for both, plain and closed lambda terms). For several other parameters (index distribution, redex search time, number of head abstractions, number of free variables) we obtain discrete limit laws. Next, for height profile with different height notions we obtain Rayleigh distribution. In addition, we present several conjectures motivated by empirical evidence. Our tools comprise analytic combinatorics and transfer theorems for infinite systems of functional equations.

Joint work with Maciej Bendkowski and Olivier Bodini.

16:45-17:30 **Jean Peyen**

*On some linear lambda term parameters* (slides)

The asymptotic analysis of linear lambda-terms can be done in a very fine way thanks to the bijection with trivaluate maps described by Bodini-Gardy-Jacquot. We are now interested in the analysis of some important parameters. We will show in this talk that the number of free variables is asymptotically Gaussian with mean in $(2n)^{1/3}$. We will also present the work in progress on other parameters.

Joint work with Olivier Bodini.

17:30-19:00 **Workshop Meeting**

9:00-9:15 **Breakfast**

9:15-10:15 **Noam Zeilberger**

*A sequent calculus for a semi-associative law*
(slides)

We introduce a sequent calculus with a simple restriction of Lambek's product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice $Y_n$.

This is based on the extended version of an article presented at FSCD 2017: https://arxiv.org/abs/1803.10080.

10:15-10:30 **Coffee Break**

10:30-11:30 **Catherine Dubois and Alain Giorgetti**

*Lambda terms and maps, formally (II)*
(slides)

At first glance lambda calculus and theory of maps (graphs embedded on a surface) seem to be two disjointed research domains. However several bijections between families of lambda terms and maps have been recently established. With the Coq proof assistant we try to mechanize a demonstration that these correspondences are bijective. In this talk we show how this research has led us to new representations of these objects. As this work is in progress we use random generators (using QuickCheck developed by Pierce et al.) to check lemmas before proving them.

11:30-12:30 **Maciej Bendkowski**

*Combinatorics of explicit substitutions*
(slides)

$\lambda\upsilon$ is an extension of the $\lambda$-calculus which internalises the calculus of substitutions. We investigate the combinatorial properties of $\lambda\upsilon$ focusing on the quantitative aspects of substitution resolution. Remarkably, an unexpected correspondence between the counting sequence for $\lambda\upsilon$-terms and famous Catalan numbers is exhibited. As a by-product, we establish effective sampling schemes for random $\lambda\upsilon$-terms. We show that typical $\lambda\upsilon$-terms represent, in a strong sense, non-strict computations in the classic $\lambda$-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e. unevaluated, under closures. Consequently, we argue that $\lambda\upsilon$ is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in $\lambda\upsilon$ and investigate the quantitative contribution of various substitution primitives.

Joint work with Pierre Lescanne.

12:30-14:30 **Lunch Break**

14:30-15:30 **Pierre Lescanne**

*Counting Environments and Closures*
(slides)

Environments and closures are two of the main ingredients of evaluation in $\lambda$-calculus. A closure is a pair consisting of a $\lambda$-term and an environment, whereas an environment is a list of $\lambda$-terms assigned to free variables. We investigate some dynamic aspects of evaluation in $\lambda$-calculus considering the quantitative, combinatorial properties of environments and closures. Focusing on two classes of environments and closures, namely the so-called plain and closed ones, we consider the problem of their asymptotic counting and effective random generation. We provide an asymptotic approximation of the number of both plain environments and closures of size $n$. Using the associated generating functions, we construct effective samplers for both classes of combinatorial structures. Finally, we discuss the related problem of asymptotic counting and random generation of closed environments and closures.

Joint work with Maciej Bendkowski.

15:30-16:00 **Coffee Break**

16:00-17:00 **Paul Tarau**

*Combinatorial Testing Techniques for Intuitionistic
Propositional Theorem Provers*
(slides)

Proving a theorem in intuitionistic propositional logic, with
*implication* as its only primitive, is known as one of the
simplest to state PSPACE-complete problem. At the same time, via
the Curry-Howard isomorphism, it is the key to finding a lambda
term that inhabits a given type, if it exists. However, as a
significant number of papers, all starting with Gentzen's **
LJ** calculus can witness it, conceptual simplicity has not come
in this case with comparable computational counterparts, facing
challenges related not only to soundness and completeness but
also to termination and scalability problems. Can a simple
solution, in the tradition of "lean theorem provers" be
uncovered that matches the conceptual simplicity of the problem,
while being able to handle randomly generated large formulas?
Could such a theorem prover be used to produce random simply
typed lambda terms comparable in size with Boltzmann samplers?
In search for an answer, working on the two sides of the
Curry-Howard isomorphism, we develop a combinatorial testing
framework, involving all-term and random term generators,
covering both simply-typed lambda terms in normal form and
implicational formulas. With its help, we derive a sequence of
minimalistic theorem provers, via declarative program
transformations steps, while working through some unexpected
challenges and highlighting connections to subtleties of type
inference mechanisms for the simply typed lambda calculus. We
use our combinatorial tester to cover soundness, completeness
and termination properties as well as scalability to large
formulas and progressively improved performance. We chose
Prolog as our meta-language. Being derived from essentially the
same formalisms as those we are covering reduces the semantic
gap and results in a surprisingly concise and efficient
declarative implementation.

Our implementation is available at https://github.com/ptarau/TypesAndProofs.

17:00-18:00 **Maciej Bendkowski**

*Polynomial tuning of multiparametric combinatorial samplers*
(slides)

Boltzmann samplers and the recursive method are prominent algorithmic frameworks for the approximate-size and exact-size random generation of large combinatorial structures, such as maps, tilings, RNA sequences or various treelike structures. In their multiparametric variants, these samplers allow to control the profile of expected values corresponding to multiple combinatorial parameters. One can control, for instance, the number of leaves, profile of node degrees in trees or the number of certain subpatterns in strings. However, such a flexible control requires an additional nontrivial tuning procedure. We propose an efficient polynomial-time, with respect to the number of tuned parameters, tuning algorithm based on convex optimisation techniques. We illustrate the efficiency of our approach using several applications of rational, algebraic and Pólya structures including polyomino tilings with prescribed tile frequencies, planar trees with a given specific node degree distribution, and weighted partitions.

Joint work with Olivier Bodini and Sergey Dovgal.

19:30- **Social Dinner**

The registration for CLA 2018 is now open!
Participation is *free of
charge*! We invite the participants to give talks of 45 minutes on
topics relevant to the theme of the workshop. Please indicate your
interest in giving a talk by sending an email to

(λx.x@lip6.fr)cla

including

- your current affiliation,
- the title of your talk
^{(*)}, and - an abstract of about 200 words
^{(*)}.

Following a selection process during the period of 3--4 May 2018, accepted talks will be announced on May 5 2018.

^{(*)} If you don't plan to give a
talk, please indicate it in the email.

The worshop will be held at the Sorbonne University (ex UPMC), Campus Pierre et Marie Curie (metro Jussieu).

On the map of the Campus Pierre et Marie Curie (metro Jussieu). There is a single entry on the campus, just near Jussieu Metro station. The entry is between the towers 46 and 56 (the red point).

**ROOM UPDATE**

Reach the tower 14 (15 is also fine). Then,
take the evelator to the 5th floor. The corridor **14/15** is open
and there you will find the room **507**.

- Cyril Banderier (Université Paris Nord)
- Maciej Bendkowski (Jagiellonian University)
- Olivier Bodini (Université Paris Nord)
- Julien Clément (CNRS, GREYC, Caen)
- Sergey Dovgal (Université Paris Nord)
- Catherine Dubois (Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise)
- Zeinab Galal (Université Paris Diderot)
- Danièle Gardy (Université de Versailles-Saint-Quentin-en-Yvelines)
- Antoine Genitrini (Sorbonne Université)
- Stefano Guerrini (Université Paris Nord)
- Alain Giorgetti (Université Bourgogne Franche-Comté)
- Bernhard Gittenberger (Technische Universität Wien)
- Katarzyna Grygiel (Jagiellonian University)
- Isabella Larcher (Technische Universität Wien)
- Pierre Lescanne (ENS Lyon)
- Florian Luca (University of the Witwatersrand)
- Philippe Marchal (Université Paris Nord)
- Mehdi Naima (Université Paris Nord)
- Le Thanh Dung Nguyen (École Normale Supérieure de Paris & Université Paris 13)
- Martin Pépin (Sorbonne Université)
- Jean Peyen (University of Leeds)
- Paul Tarau (University of North Texas)
- Michael Wallner (Université de Bordeaux)
- Marek Zaionc (Jagiellonian University)
- Noam Zeilberger (University of Birmingham)

Below you can find details regarding some of the most recent CLA editions:

- 2017, Göteborg (Sweden)
- 2016, Novi Sad (Serbia)
- 2015, Lyon (France)
- 2012, Kraków (Poland)
- 2011, Wien (Austria)

CLA 2018 is organized jointly by Laboratoire d'Informatique de Paris-Nord and Laboratoire d'Informatique de Paris 6.

Main organizers are:

- Maciej Bendkowski, (λx.x@tcs.uj.edu.pl)bendkowski
- Olivier Bodini, (λx.x@lipn.univ-paris13.fr)olivier.bodini
- Antoine Genitrini, (λx.x@lip6.fr)antoine.genitrini