10th Workshop
Computational Logic and Applications
Göteborg, Sweden, 18-19 May 2017
| 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 |
| 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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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)
Abstract:
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.