Editorial team – Page 23

The workshop will be held at the Departamento de Computación of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!

10:00-10:15 Sergio Yovine and Eduardo Bonelli
Opening remarks

10:15-10:50 Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

10:50-11:25 Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

11:25-11:40 Coffee break

11:40-12:15 Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

12:15-12:50 Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

12:50-14:00 Lunch

14:00-14:35 Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

14:35-15:10 Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

15:10-15:25 Coffee break

15:25-16:00 Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

16:00-16:15 Sergio Yovine and Eduardo Bonelli
Closing remarks

————————————————————————————————————–
Abstracts of talks:

Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.

Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time. While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4).
Joint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong

Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.

Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

Proof assistants like Coq are now eminently effective for formalizing “research-grade” mathematics, verifying serious software systems, and, more broadly, enabling researchers to mechanize and breed confidence in their results. Nevertheless, the mechanization of substantial proofs typically requires a significant amount of manual effort. To alleviate this burden, proof assistants typically provide an additional language for tactic programming. Tactics support general-purpose scripting of automation routines, as well as fine control over the state of an interactive proof. However, for most existing tactic languages (e.g., ML, Ltac), the price to pay for this freedom is that the behavior of a tactic lacks any static specification within the base logic of the theorem prover (such as, in Coq, a type). As a result of being untyped, tactics are known to be difficult to compose, debug, and maintain.

In my thesis I developed two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. Both approaches rely heavily on the unification algorithm of Coq, which is a complex mixture of different heuristics and has not been formally specified. Therefore, I also build and describe a new unification algorithm better suited for tactic programming in Coq. In this talk I describe the high level achievements of my work and introduce in depth Mtac, a new programming language for typed tactic programming in Coq.

Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\mathcal K}(\alpha)$ of the fractional parts of the multiples of a real $\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\mathcal K}(\alpha)$, and is useful to study the pseudo-randomness of the sequence ${\mathcal K}(\alpha)$ for a random input $\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\alpha$ is a random real, and the case when $\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\alpha$ plays an important rôle. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\infty$ and the unconstrained case $M = \infty$. Joint work with Brigitte Vallée, CNRS and Université de Caen, France.

Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.

Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.