A Gentle Introduction to Matching Logic and its Applications

Speaker: Dorel Lucanu

Tuesday, 28 March 2023, 14:00, 1Z56 New date: Wednesday, 29 March 2023, 14:00, hybrid

Abstract: Matching Logic (ML) allows to uniformly specify and reason about programming languages and properties of their programs. It was developed as a logical foundation of the K framework.

ML is expressive enough to specify all properties within various logical systems such as FOL, separation logic,  lambda-calculus, (dependent) type systems, and modal  mu-calculus. In particular, it supports operational semantics (term rewriting) and axiomatic semantics (Hoare triples). ML has a sound  fixed Hilbert-style proof system that supports formal reasoning for all specifications. In this talk we give a gentle introduction to (Applicative) Matching Logic [3], we show how the initial algebraic semantics can be encoded as ML theories [4], and how ML is used to formaly define programming languages semantics and program properties.



Séminaires antérieurs

Keynote: The Future of Model-based Testing

Speaker: Jan Peleska, Universität Bremen, Saarbrücken, Germany

Friday 17 March 2023, 14:00, Room 1Z56

Abstract: Since the 1970s, model-based testing (MBT) has been comprehensively investigated in the research communities, and its industrial application has been fostered for at least two decades. Though convincing success stories about MBT have been published, we have to admit that its acceptance in industry is still not as good as it should be. This is reflected, for example, by the facts that commercial MBT tools are not selling as well as had been originally envisaged by the “campaigners of MBT” (such as myself) and that MBT has not been integrated into the verification plans of the key players in the embedded systems world. Read more...

Strategy Complexity of Zero-Sum Games on Graphs

Speaker: Pierre Vandenhove

Tuesday, 14 Mars 2023, 14:00, 1Z77

Abstract: In this seminar, I will present the results obtained as part of my PhD thesis cosupervised by Patricia Bouyer at LMF and Mickael Randour at Université de Mons (Belgium). This seminar precedes my thesis defense which will take place in Mons in April. I include here a short abstract; more details are available at my website.

We study zero-sum turn-based games on graphs. Such games can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. The synthesis problem consists in automatically building a controller for the system that guarantees a given objective no matter what happens in the environment, that is, a winning strategy in the derived game.


The Frobenius Anatomy of Distributed Quantum Protocols

Speaker: Alexis Toumi, email:

Tuesday, 10 January 2023, 14:00, Salle 1Z31

Abstract: Distributed consensus and leader election are two communication problems that quantum computers can solve in a deterministic way, while classical computers can only solve them probabilistically. These two quantum protocols can in fact be put in one-to-one correspondance with the GHZ and W states, the only two ways to entangle three qubits (up to LOCC, local operations and classical communication). In this talk, we will give an abstract formulation of quantum consensus and leader election in terms of spiders, also known as Frobenius algebras. In both cases, a single equation allows to create global entanglement from local interactions: spider fusion. We will conclude with some applications to quantum natural language processing (QNLP) where spiders allow to formalise the notion of anaphora and co-reference: we can compute a global meaning for text as the entanglement of local meanings for sentences.

An Abstraction of the Unit Interval with Denominators

Speaker: Marco Abbadini

Wednesday, 4 January 2023, 14:00, visio link:

Abstract: Compact Hausdorff spaces are the topological abstraction of the unit interval [0,1] (in a sense that can be made precise). Let us now equip the unit interval with the "denominator map" den: [0,1] -> N that maps a rational number to its denominator and an irrational number to 0. We characterize the abstraction of [0,1] that takes into account both the topology and the denominator map.

(We use this result to provide a representation theorem for a class of lattice-ordered groups, generalizing a result of M.H. Stone (1941).)

Keynote: The Skolem Landscape

Speaker: Joël Ouaknine, Max Planck Institute for Software Systems, Saarbrücken, Germany

Tuesday, 13 December 2022, 14:00, Room 1Z56

Abstract: The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, the decidability of the Skolem Problem has been open for nearly a century! In this talk, I will present a survey of what is known on this problem and related questions, including recent and ongoing developments.

Consistent Circuits for Indefinite Causal Order

Speaker: Augustin Vanrietvelde, LMF

Tuesday, 6 December 2022, 14:00, Room 1Z53

Abstract Over the past decade, a number of quantum processes have been proposed which are logically consistent, yet feature a cyclic causal structure. However, there exists no general formal method to construct a process with an exotic causal structure in a way that ensures, and makes clear why, it is consistent. Here we provide such a method, given by an extended circuit formalism. This only requires directed graphs endowed with boolean matrices, which encode basic constraints on operations. Our framework (a) defines a set of elementary rules for checking the validity of any such graph, (b) provides a way of constructing consistent processes as a circuit from valid graphs, and (c) yields an intuitive interpretation of the causal relations within a process and an explanation of why they do not lead to inconsistencies. We display how several standard examples of exotic processes, including ones that violate causal inequalities, are among the class of processes that can be generated in this way; we conjecture that this class in fact includes all unitarily extendible processes.

Programming with (Discrete and Continuous) Ordinary Differential Equations

Speaker: Olivier Bournez, LIX, École Polytechnique

Tuesday, 15 November 2022, 14:00, Room 1Z14

The Analog ThingA

Abstract: Initially motivated by understanding the computational power of various continuous-time analog models of computations, several characterizations of  complexity and computability classes have been obtained recently using ordinary differential equations. Basically, each class is characterized as the class of functions containing some basic functions, and closed by composition and various natural schemas or constructions, based on ordinary differential equations.  

This means for one direction of these proofs that we can program with ordinary differential equations.

We will provide a review of some of these recent results, and some applications. We will mainly focus on their discrete counterpart, also known as discrete ordinary differential equations, or finite differences. 

Formal Security Proofs in a Post-Quantum World

Speaker: Charlie Jacomme, Inria, Paris

Tuesday, 22 November 2022, 14:00, Room 1Z76


Abstract: In the recent years, formals methods for security and their associated tools have been used successfully both to find novel and complex attacks on many protocols [A] and to help in their standardization process. They however face a new challenge with the increasing probability of quantum computers coming into the real-world: we need to be able to provide guarantees against quantum attackers.

In this talk, we will first present a broad overview of formal methods, outlining what is the general goal of the field. We will then focus on the post-quantum issue by presenting the corresponding concrete challenges, and thus multiple ways current computational proofs of security (proof for any Polynomial Time Turing Machine attacker) can fail against a quantum attacker. We will then present the first-order logic over which Squirrel is built, the BC logic, and show based on the first part where it fails at post-quantum soundness. In a third part, we will finally present our contribution: how we made the logic and thus the Squirrel prover post-quantum sound.

Machine Learning and Autoformalisation

Speaker: Anthony Bordg, University of Cambridge

Thursday, 16 November 2022, 14:00, room 3U42


In this talk, I will describe our early achievements and future plans for increasing, through machine learning, Isabelle's competitiveness.

Verification and Synthesis of Complete Test Generation Algorithms for Finite State Machines

Speaker: Robert Sachtleben, University Bremen, Germany.

Tuesday 25 Oct 2022, 14:00, Room 1Z76

Abstract: Complete test suites are of special interest in the field of model-based testing, as they guarantee high fault detection capabilities. The variety and complexity of proposed strategies, their implementations, and their corresponding completeness arguments, however, impede thorough manual verification and practical employment.

We present a novel approach to the verification and synthesis of such strategies for models specified using finite state machines. First, we unify the presentation of several such strategies into a single framework implemented as a higher order function, which represents their shared high-level behaviour. Next, we model this framework in the interactive theorem prover Isabelle. Completeness proofs over frameworks are decoupled from concrete implementations of their parameters by suitable interfaces. This approach enables the reuse of proofs between similar strategies and simplifies implementations and completeness proofs of new variations on already handled strategies. Finally, we generate provably correct implementations of the considered test strategies. It is shown that these exhibit comparable performance to a manually developed C++ library for certain inputs.