10th Workshop

Computational Logic and Applications

Göteborg, Sweden, 18-19 May 2017

Thursday 18 May (Room EDIT 3364)

Time Speaker Talk
10:00-11:00 Leonidas Lampropoulos Testing before Proving in the Coq Proof Assistant
11:00-11:15 Coffee break
11:15-12:00 Alberto Momigliano Property-based testing programming languages artifacts
12:00-13:15 Lunch break
13:15-14:00 Maciej Bendkowski Properties of random lambda and combinatory logic terms
14:00-14:45 Pierre Lescanne Quantitative aspects of linear and affine closed lambda terms
14:45-15:00 Coffee break
15:00-16:00 Break-out session
16:00-16:45 Sergey Dovgal Enumeration of closed lambda-terms
16:45-17:30 Noam Zeilberger Some enumerative, topological, and algebraic aspects of linear lambda calculus

Friday 19 May (Room EDIT 8103)

Time Speaker Talk
10:00-10:45 John Hughes Random Distributions for Property-Based Testing
10:45-11:00 Coffee break
11:00-11:45 Paul Tarau On Type-holding and type-repelling lambda-term skeletons, with applications to all-term and random-term generation of simply-typed closed lambda terms
11:45-13:00 Lunch break
13:00-13:30 Simon Poulding Generating Structured Test Data with Specific Properties using Metaheuristic and Nested Monte-Carlo Search
13:30-14:15 Bernhard Gittenberger Enumerating Lambda Terms by Weighted Length of Their de Bruijn Representation
14:15-14:30 Coffee break
14:30-15:15 Sergey Dovgal Shifting the phase transition in random 2-CNF satisfiability
15:15-16:00 Open discussion session (notes by Martin Berger)


Invited talk

Speaker: Leonidas Lampropoulos, University of Pennsylvania

Title: Testing before Proving in the Coq Proof Assistant (slides)

Formal verification provides strong guarantees about the absence of bugs in software artifacts; however, the verification process is still long and expensive, and requires a lot of manual effort from the prover. Random testing can facilitate this process by revealing bugs early on, before the prover has wasted time attempting to prove a false theorem. In this talk, we present QuickChick, a QuickCheck-inspired random testing tool for the Coq proof assistant. We give a high level overview of testing and proving in Coq using a simple example. Finally, we sketch our ongoing research efforts to automatically produce correct generators for random data satisfying complex inductive propositions.

Contributed talks:

Speaker: Pierre Lescanne, LIP ENS de Lyon

Title: Quantitative aspects of linear and affine closed lambda terms (slides)

Affine lambda-terms are lambda-terms in which each bound variable occurs at most once and linear lambda-terms are lambda-terms in which each bound variable occurs once. and only once. In this paper we count the number of closed affine lambda-terms of size $n$, closed linear lambda-terms of size $n$, affine $\beta$-normal forms of size $n$ and linear $\beta$-normal forms of size $n$, for different ways of measuring the size of lambda-terms. From these formulas, we show how we can derive programs for generating all the terms of size $n$ for each class. The foundation of all of this is specific data structures, which are contexts in which one counts all the holes at each level of abstractions by lambdas.

Speaker: Maciej Bendkowski, Jagiellonian University

Title: Properties of random lambda and combinatory logic terms (slides)

In this overview presentation, we survey recent quantitative results in $\lambda$-calculus and combinatory logic, focusing on properties of large `typical' terms as well as thier effective uniform generation. We discuss utilised analytic techniques, uniform property-focused term generation methods and their current limitations. Finally, we review open problems and challenges connected to random $\lambda$-terms and combinatory logic terms.

Speaker: John Hughes, Chalmers University/Quviq AB

Title: Random Distributions for Property-Based Testing (slides)

Property-based testing tools, such as QuickCheck, test software against formal specifications in the form of universally quantified properties, by generating random test cases and checking the properties in each case. It has been used in Haskell since 2000, and commercially at Quviq since 2006, and the basic idea has been emulated for more than 30 other programming languages. Effective testing—finding faults quickly—depends very much on the distribution with which test cases are generated. But what is a “good” distribution for testing? It’s tempting to think that a uniform distribution should a priori be the most suitable. I’ll give examples from our experience to show that this is definitely not the case, especially for test cases that must satisfy complex invariants. Instead, in practice, test case distribution is usually tuned by hand; I’ll illustrate some of the techniques used to do so. While code coverage is a fairly poor criterion for test case generation, I’ll describe a related criterion and show how we use it to tune test case generation from finite-state machine models semi-automatically. Finally I’ll describe some adaptive methods for learning from previous tests, with a performance comparison between RANDOOP (a well established random testing tool) and an adaptive method of our own.

Speaker: Alberto Momigliano, Dipartimento di Informatica, Università degli Studi di Milano, Italy

Title: Property-based testing programming languages artifacts (slides, code)

We report on work in progress in building an environment for the the validation of the meta-theory of programming languages artifacts, for example the correctness of compiler optimizations; the basic idea is to couple property-based testing with binders-aware functional programming as the meta-language for specification and testing. Treating binding signatures and related notions, such as new names generation, alpha-equivalence and capture-avoiding substitution correctly and effectively is crucial in verification and validation of PL (meta)theory. We use Haskell as our meta-language, since it offers various libraries for both random and exhaustive generation of tests, as well as for handling binders. We validate our approach on benchmarks of mutations presented in the literature, pertaining to type soundness and information flow security, and some examples of code "in the wild". In the former case, not only did we very quickly (re)discover all the planted bugs, but we achieved that with very little configuration effort with comparison to the competition. In the second case we located several simple bugs that had survived for years in shared (academic) code. While this experience points to the usefulness of PBT, in alternative or prior to full verification for semantic engineering of programming languages, we currently fall short of locating known "deep" bugs such as the one that lead to the value restriction in SML. We discuss why this is the case and what we plan to do about it.

Speaker: Noam Zeilberger, University of Birmingham

Title: Some enumerative, topological, and algebraic aspects of linear lambda calculus (slides)

Enumeration of graphs on surfaces (or "maps") is an active topic of research in combinatorics, with links to wide-ranging domains such as algebraic geometry, knot theory, and mathematical physics. In the last few years, it has also been found that map enumeration is related to the combinatorics of lambda calculus, with various well-known families of maps in 1-to-1 correspondence with various natural families of linear lambda terms. In the talk I will begin by giving a brief survey of these enumerative connections, then use those to motivate a closer look at the surprisingly rich topological and algebraic properties of linear lambda calculus.

Speaker: Paul Tarau, University of North Texas

Title: On Type-holding and type-repelling lambda-term skeletons, with applications to all-term and random-term generation of simply-typed closed lambda terms (slides)

Lambda terms in de Bruijn notation are Motzkin trees (also called binary-unary trees trees) with indices counting up to a binder among the lambdas on the path to the root labeling their leaves. Define the skeleton of a lambda term as the Motzkin tree obtained by erasing the de Bruijn indices labeling their leaves. Then, given a Motzkin tree, one can ask if it is the skeleton of at least one closed lambda term. More interestingly, one can ask the same question for simply-typed closed terms. A type-holding Motzkin tree is one for which it exists a simply-typed closed term having it as its skeleton. A type-repelling Motzkin tree is one for which no simply-typed closed term exists having it as its skeleton. We explore some of their properties and derive, with their help, faster than previously known all-term and random term generators for simply-typed closed lambda terms. We describe a creative use of a Boltzmann sampler for first generating type-holding Motzkin trees and then decorating them with de Bruijn indices, in parallel, to simply-typed closed lambda terms. Parallel algorithms for counting or generating all simply-typed terms of a given size require careful load balancing, given the uneven distribution of these terms for different constructor densities. We describe algorithms that ensure full usage of all worker threads, supported by experimental data on a machine with a large number of CPU units.

Speaker: Bernhard Gittenberger, TU Wien, Austria

Title: Enumerating Lambda Terms by Weighted Length of Their de Bruijn Representation (slides)

John Tromp introduced the the so-called binary lambda calculus as a way to encode lambda terms by means of 0-1-strings. Later, Grygiel and Lescanne conjectured that the number of binary lambda terms which have $m$ free indices and are represented by a binary word of length n deof size $n$, i..e they are of size $n$, is asymptotically smaller than $n^{-3/2}\tau^{-n}$ for $\tau \approx 1.963448\ldots$. We generalize the proposed notion of size and show that for several classes of lambda terms, including binary lambda terms with $m$ free indices and other notions of size having been proposed in the literature, the number of terms of size $n$ is in fact asymptotically equal to $C n^{-3/2} \rho^{-n}$ with some class dependent constant $\rho$, which in particular disproves the above mentioned conjecture. A lower and upper bound of that form, which are numerically very tight to each other, can be obtained by a sort of bootstrapping procedure. By approximation the generating function for large $m$ by its limiting function (corresponding to the case $m=\infty$) it is eventually possible to derive the actual existence of such a constant $C$. The method can be extended further to allow the analysis of parameters of lambda terms, like the number of abstractions or the number of variables in a typical large lambda term. Moreover, the approach can be used to design Boltzmann samplers for lambda terms, an efficient method in order to generate lambda terms of a given size uniformly at random. Using these samplers, it is possible to generate and draw a random lambda term of size 1 million within a couple of minutes using a laptop with a 2.6GHz CPU.

Speaker: Sergey Dovgal, LIPN, Université Paris-13

Title: Enumeration of closed lambda-terms (slides)

In the current talk we introduce the 'natural counting of lambda-terms' notion framework of Gittenberger and Gołębiewski, and study distributions of several statistics of plain and closed lambda-terms such as the number of variables, average value of indices, number of redexes or the number of closed sub-terms. Some extremal statistics are also investigated: the unary height of a lambda-term, maximal lambda-run, maximal value of de Bruijn variable index. Using tools from analytic combinatorics we show that the statistical behaviour of such lambda-terms is similar to that of trees. Some insights into random generation are also addressed. Open problems can be discussed. Joint work with Maciej Bendkowski and Olivier Bodini.

Speaker: Simon Poulding, Blekinge Institute of Technology

Title: Generating Structured Test Data with Specific Properties using Metaheuristic and Nested Monte-Carlo Search (slides)

Software acting on highly-structured data structures can be challenging to test: it is difficult to generate diverse test data that satisfies structural constraints while simultaneously exhibiting properties, such as a particular size, that the test engineer believes will be effective in detecting faults. GödelTest is a framework for generating such data structures at random. It combines non-deterministic generators — written by the test engineer in a general-purpose programming language — that specifies valid structures, with a choice model that makes random choices at the points of non-determinism. We show that by applying metaheuristic search and nested Monte-Carlo search (a form of Monte-Carlo Tree Search) to optimise the choice model, test data possessing effective properties can be generated efficiently.

Speaker: Sergey Dovgal, LIPN, Université Paris-13

Title: Shifting the phase transition in random 2-CNF satisfiability (slides)

The prominent result of Bollobàs, Borgs, Chayes, Kim, and Wilson is that for random conjunctive normal forms (2-CNF) with $n$ variables and $m$ clauses, when $m < n (1-\alpha)$, 2-CNF is satisfiable with high probability, and when $m > n(1+\alpha)$, 2-CNF is unsatisfiable with high probability. We introduce a more general model, in which the number of clauses that contain each variable, belongs to a given set $S$. For each $S$ there exists a computable constant $r$ such that the point of phase transition is shifted from $m = n$ to $m = r n$. Random generation of such 2-CNF's will be also discussed. This result is a consequence of numerous properties of random graphs within degree constrained framework which was obtained jointly with Vlady Ravelomanana.