Stable event structures and their duality with prime algebraic domains (arising as partial orders of configurations) are a landmark of concurrency theory, providing an elegant characterisation of causality in computations. They have been used for defining a concurrent semantics of several formalisms, from Petri nets to linear graph rewriting systems, which in turn lay at the basis of many visual frameworks. Stability however is restrictive for dealing with formalisms where a computational step can merge parts of the state, like graph rewriting systems with non-linear rules, which are needed to cover some relevant applications (such as the graphical encoding of calculi with name passing). We characterise, as a natural generalisation of prime algebraic domains, a class of domains that is well-suited to model the semantics of formalisms with fusions. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result.

Dans de nombreux écosystèmes de langages de programmation, les développeurs dépendent de plus en plus de dépendances externes en open source, disponibles via des gestionnaires de paquets. Les paquets clés qui ne sont pas maintenus présentent un risque pour les projets qui en dépendent ainsi que pour les écosystèmes. Par conséquent, des initiatives communautaires peuvent émerger au sein des écosystèmes pour résoudre ce problème en adoptant les paquets clés ayant des problèmes de maintenance. Dans mon exposé, je présenterai les résultats de l'article coécrit avec Jean-Rémy Falleri et récemment publié dans Empirical Software Engineering intitulé “A Grounded Theory of Community Package Maintenance Organizations”. Le but de celui-ci était de construire une théorie de ces organisations (CPMO), notamment leur émergence et leur mode de fonctionnement. Pour ce faire, nous avons utilisé une méthodologie qualitative appelée Grounded Theory. Nous avons analysé des documents existants provenant de plusieurs CPMO, tels que des documentations et des discussions sur des forums publics, complétés par des entretiens avec des initiateurs de CPMO. Je parlerai également de mon application de ce modèle d'organisation à l'écosystème Coq, avec la création de l'organisation Coq-community, et de l'expérience acquise par ce biais.

Memory management is notoriously difficult in a concurrent setting. The presence of garbage collection greatly simplifies the life of the programmer, eradicating many memory-related bugs. However, the heap space usage of garbage-collected programs can be tricky to understand and reason about, as there is no explicit program point where space is reclaimed.

We recently presented a Separation Logic with Space Credits to reason about heap space under garbage collection in a high-level, yet sequential, language.

In this talk, we scale up to a concurrent language. For this purpose, we introduce new “pointed-by-thread” assertions, which keep track of the existence of stack-to-heap pointers in a reasonably lightweight manner. We illustrate our approach on a range of examples, including the standard lock-free Treiber's stack, and unveil its surprisingly high heap memory bounds in the presence of garbage collection.

PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations.

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

“Smart contract” are software whose byte code is executed by node validators/block makers operating a block chain. These “open^2” code (open source + open execution layer) provide an entirely transparent execution stack (on public blockchains) that is foreseen to complement (or even replace) most standard trusted third party based transactions (i.e based on trusting a bank, or a notary for settlement) in a near future.

In this workgroup I will introduce basic concepts of the Ethereum Virtual Machine (EVM) and Solidity (the most used programming language on top of the EVM). To illustrate these concepts I will describe Mangrove, a decentralised exchange protocol designed for the EVM. This should allow us to discuss difficulties and technical solutions that naturally arise when designing smart contracts managing user funds. In particular we will discuss current limitations of solidity and the need for better programming paradigms for critical onchain softwares.

Depuis 2013, le PAMAL (Preservation & Art – Media Archaeology Lab), qui devient en 2019 le PAMAL_Group, associe création et recherche dans le champ de l’archéologie des média. PAMAL_Group crée ses propres œuvres à partir d’œuvres d’art numérique disparues ou fortement endommagées en raison de l’obsolescence des logiciels et matériels informatiques. Ses travaux cherchent à rendre sensible la vulnérabilité d’un art fortement dépendant des logiques industrielles. Toutes les œuvres que le collectif reconstruit sont au plus près des matérialités d’origine. Le 13 avril, les deux membres fondateurs du PAMAL_Group viendront présenter les derniers projets télématiques du collectif, récemment exposés au Centre Pompidou et au ZKM (Zentrum für Kunst und Medien de Karlsruhe).

Dans cet exposé très informel à propos d'un travail en cours, je souhaiterais discuter de différents styles pour définir (en Coq) la sémantique d'un langage de programmation. Une de mes motivations est d'obtenir une sémantique au moins partiellement exécutable dans Coq et d'en tirer un mécanisme d'exécution symbolique qui pourrait être exploité dans un système de vérification de programmes.

Au cours de l'exposé, je présenterai deux styles de sémantique (pour un langage sans effets de bord, hormis divergence et plantage), et au-dessus de chacun d'eux, je construirai une logique de Hoare. Le premier style, “monadique jusqu'au bout”, reproduit des idées que l'on trouve dans la littérature: un premier interprète est exprimé dans une monade libre bien choisie, puis, dans un second temps, les habitants de cette monade sont traduits dans d'autres monades (monade des interaction trees; monade de spécification). Le second style, “à pas amples”, est hybride: dans une couche inférieure, on conserve le même interprète monadique, exprimé dans la monade libre; dans une couche supérieure, on raisonne à l'aide d'une sémantique opérationnelle à petits pas. J'aimerais recevoir des commentaires et suggestions du public afin de prévoir les prochaines étapes: ajout du non-déterminisme, du parallélisme, de l'état mutable, puis construction d'une logique de programmes de la famille Iris.

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is mainly carried out in the ML community, while research in ML verification is mostly carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by presenting our recent and ongoing work on interpretability-aware verification of ML software. On the one hand, we show how verification can aid interpretability by providing a new feature importance measure for support vector machines. On the other hand, we discuss how interpretability can guide verification by proposing a new saliency-guided robustness verification problem for deep neural networks. We conclude with plans and perspectives on future work.

https://www.irill.org/events/2023/event20230202.html

Assembling off-the-shelf or independently-developed components into a system is a common practice. Although a few useful tools exist, this remains manual, ad-hoc, complex, labour-intensive, and error-prone.

Varda provides a higher level of abstraction. An Varda program describes how to compose components into a safe architecture. The programmer isolates an off-the-shelf (OTS) component behind an Varda shield, which specifies its interface, its protocol, and its pre- and post-conditions.

Components can be logically nested, providing encapsulation boundaries; the outer component orchestrates its inner components. It can intercept communication, as a general mechanism to compute over components and messages. Varda provides strong guarantees, enforcing the specification by static analysis, by run-time checks, and by sandboxing. To be useful, Varda takes a pragmatic approach. An OTS adaptor can contain non-Varda code (e.g., Java). Varda provides control over properties such as elasticity, placement, and inlining. Varda supports non-stop execution thanks to supervision mechanisms.

Kyber is a key-encapsulation mechanism (KEM), whose security is based on the hardness the Module-LWE problem. It is the only KEM that has been selected by the NIST Post-Quantum Cryptography project, and will be part of NIST’s first post-quantum cryptography standard. Hakyber, a formally verified implementation of Kyber, has been developed. Hakyber is written in Jasmin, and formally verified in EasyCrypt.

EasyCrypt has already been used to prove the correction of implementations of cryptographic primitives, such as of ChaCha20-Poly1305. This proof is done by “game hopping”: the correction of a naive implementation of the primitive is proven using EasyCrypt’s probabilistic Hoare logic (pHL), and it is shown to be equivalent to gradually more optimized implementations using EasyCrypt’s probabilistic relational Hoare logic (pRHL).

Hakyber differs from the cryptographic primitives formalized in EasyCrypt by the complexity of the mathematical structures involved in it’s correctness an security proofs. In particular, it’s correction proof involves polynomials over finite fields, quotient rings and Number Theoretic Transforms (NTTs), variants of the Fourier transform used in fast polynomial multiplication algorithms.

The correction proof of Hakyber’s NTT is one of the trickiest parts of the total correction proof. We will discuss the issues we encountered in this proof, the solutions we used to overcome them, and current and planned developments of EasyCrypt that were motivated by these issues.

In particular, we will talk about the theories developed to deal with equivalence proofs of nested for loops, as well as those describing algebraic hierarchies using EasyCrypt’s clone mechanism. We will then present the planned replacement for these theories, using EasyCrypt’s annotations and type class mechanism respectively.

I will present work in progress on a research programs aiming to compile efficiently automata-model of computation using vectorial instructions and bit-level paralellism.

The compilation procedure relies on algebraic automata theory that will be gently introduced. Some complexity related consideration will also provides insight on what to expect and what is (probably) hopeless to compile efficiently.

It is usually considered that the security of network protocols is a difficult problem that should be reserved to specialists (“don't design your own crypto”). Yet, in 2018, together with Clara Dô and Weronika Kołodziejak, we set out to design a simple and provably correct security mechanism for the Babel routing protocol.

Much to our surprise, our work passed successfully the IETF's security review, and was subsequently published as RFC 8967. In the Spring of 2022, however, it was discovered that even though our protocol had been proved correct, it was failing in a small number of “real” networks, which turned out to violate one of the assumptions made in our proof.

In this talk, I will first describe the properties that are expected from a security mechanism. I will then show the proof of correctness of the security mechanism described in RFC 8967, and show the assumptions that it makes about the network. Finally, I will describe how these assumptions turned out to be incorrect, and how we managed to fix the protocol in a backwards compatible manner.

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

The energy of a system of atoms is approximately a function of the position of the nuclei. This function is called the potential energy surface (PES). Knowledge of the PES is fundamental in ab-initio sciences but unfortunately, it cannot be computed in closed form. As a result, an important problem is that of exploring the PES to discover important features, such as local minima.

In this talk, I will introduce an experimental probabilistic programming language designed to facilitate the exploration of PES. In this language, the semantics of a program is a probability distribution over PES. The objective of the compiler is to generate an optimizer that combines solvers from machine learning and quantum chemistry to discover local minima of the PES. While much of this language and compiler is routine, we will see that the principle of conservation of energy brings about genuinely interesting compilation problems.

We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads. See https://arxiv.org/pdf/2202.01344.pdf

Parmi les techniques de détection automatisée de tests, le fuzzing gagne chaque année en popularité.

Cette technique permet d'explorer rapidement la surface d'un programme grâce à la génération automatique rapide de cas de tests, parfois guidée par exemple par des mesures de couverture.

En revanche, dès que le programme contient des conditions spécifiques (par exemple, x = 0x42, où x a été lu depuis l'entrée utilisateur), la probabilité qu'un fuzzeur génère une solution est assez faible.

On propose d'améliorer les perfomances du fuzzeur AFL en le combinant avec une analyse symbolique, qui analysera les traces des cas de tests générés, pour identifier ces conditions (par exemple, on aurait input[0] = 0x0042). On en déduit des prédicats de chemins sous-approximés, qu'on appelle “facilement énumérable”, et dont les solutions sont directement générées par notre fuzzeur modifié.

L'outil ainsi créé, ConFuzz, est intégré à la plateforme d'analyse de code binaire Binsec, développée au CEA List, et a été testé sur LAVA-M, un banc de test standard en fuzzing.

In practice, the popular proof assistants based on type theory (Coq, Agda, Lean) all require users to navigate around performance issues and bottlenecks in sufficiently large or complex codebases. I hypothesize some common performance issues and try to address them in a minimal implementation, called “smalltt”. One goal is to have a concrete data point for what kind of performance is achievable in the presence of the basic convenience features of pattern unification and implicit arguments. Another goal is to develop general solutions which plausibly scale to production-strength systems without losing too much performance, and also allow fine-tuning based on more realistic codebases.

Nested datatypes have been widely studied in the past 25 years, both theoretically using category theory, and practically in programming languages such as Haskell. They consist of recursive polymorphic datatypes where the type parameter changes throughout the recursion. They have a variety of applications such as modelling memory or constraints over regular datatypes.

Our work focuses on a specific subset of nested datatypes which we call Linked Nested DataTypes (LNDT), and which induces the definition of some regular datatypes, such as List and Maybe, as well as some nested datatypes, such as Nest and Bush. LibNDT is a core library, developed both in Coq and Agda, which focuses on the set of constructs that can be spread directly from the parameter on which a specific LNDT is built to the LNDT itself (For instance, List is built with the identity parameter). These spreadable elements are of two kinds, functions, such as folds and map, and properties such as the congruence of map or Any and All (existential and universal satisfaction of a predicate inside a LNDT).

In this presentation, we explain the thought process behind the creation of this specific subset of nested datatypes, and we present different concrete LNDTs, as well as our set of spreadable elements over them. We conclude by an open discussion about various thoughts related to our work.

Despite significant progress in the formal verification of security-critical components like cryptographic libraries and protocols, the secure integration of these components into larger unverified applications remains an open challenge. The first problem is that any memory safety bug or side-channel leak in the unverified code can nullify the security guarantees of the verified code. A second issue is that application developers may misunderstand the specification and assumptions of the verified code and so use it incorrectly. In this presentation, we propose a novel verification framework that seeks to close these gaps for applications written in Rust. At the heart of this framework is hacspec, a new language for writing succinct, executable, formal specifications for cryptographic components. Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then replace this specification with a verified implementation before deployment. We present the hacspec language, its formal semantics and type system, and describe a translation from hacspec to F*. We evaluate the language and its toolchain on a library of popular cryptographic algorithms.

Dans le langage OCaml, les constructeurs de types algébriques sont représentés par des pointeurs vers des blocs mémoire. Cette représentation uniforme a de nombreux avantage, mais les utilisateurs aimeraient parfois des représentations plus compactes.

Dans ce travail, en collaboration avec Nicolas Chataing et Stephen Dolan, nous étudions la possibilité de “déboîter” certains constructeurs – si l'utilisateur le demande au moment de leur définition – c'est-à-dire de ne pas les représenter en mémoire du tout. Dans certains cas, effacer les constructeurs introduirait des confusions entre valeurs différentes, et il faut donc rejeter la demande. Nous avons donc conçu une analyse statique pour détecter ces confusions; la question de la terminaison de cette analyse est intéressante.

(TBA)

The forthcoming edition of POPL will feature a rather elegant piece [https://www.cl.cam.ac.uk/~ds709/agda-soas/formal-metatheory-of-soas.pdf] by M. Fiore and D. Szamozvancev on the implementation of intrinsic syntaxes in type theory, using the usual categorical tools (initial algebra semantics, presheafs, etc.) as an effective blueprint for the construction.

I propose (rather: Adrien has volunteered me) to show up with an Agda buffer and offer a live tour and commentary of the code.

We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses “occurrence typing”. The latter is a typing technique that takes into account the result of type tests to assign different types to a same expression when it occurs in different branchings of the test.

To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

Cython+ est un projet expérimental d'extension du compilateur Cython sur lequel je travaille depuis un an et demi.

Cython permet de joindre Python et C/C++ au sein d'un même langage. L'intérêt majeur de Cython est qu'il rend facile l'utilisation de code C/C++ comme back-end de code Python. On peut ainsi contourner le GIL de Python (le verrou global qui ne permet qu'à un seul thread à la fois d'exécuter du bytecode Python dans l'interpréteur CPython).

Avec Cython+, nous étendons les possibles de Cython sur trois aspects: 1. Tout d'abord, nous introduisons un système d'objets utilisables sans le GIL en exécution multi-thread sur plusieurs coeurs. La gestion de la mémoire est automatique comme en Python grâce à un comptage de références atomique. De plus une couche de compatibilité transparente en fait de vrais objets Python manipulables en tant que tels directement depuis l'interpréteur Python. 2. De plus, nous ajoutons à cela un modèle d'exécution asynchrone à base d'acteurs et une implémentation d'un scheduler inspiré par celui de Go. 3. Enfin, nous sommes en train d'explorer un système de types pour la thread safety inspiré par ceux de Pony et Rust.

Reactive systems, which are omnipresent from airplanes to videogames, execute in continuous interaction with their environment. Functional reactive programming (FRP) aims to describe these systems as mathematical functions between the infinite streams of their inputs and outputs.

Several lines of research have enriched this approach with strong type systems: works based on Nakano's guarded recursion use type-theoretical modalities to guarantee productivity. While this approach has its benefits, many of such domain specific functional languages fail to have a runtime suitable for resource-scarce environments. Such environments usually use the synchronous programming paradigm, which uses more specialized methods, but gives strong guarantees on the efficiency of the program.

In this presentation, we aim to present a recent synthesis between the two approaches by describing how a FRP language can be given a semantics in the synchronous style. We will then investigate the potentially deeper connections between synchronous programming and FRP.

In this introductory session of the reading group, we will read, discuss and dissect the following two papers

1. Learning to Prove Theorems via Interacting with Proof Assistants
2. TacTok: semantics-aware proof synthesis

In the context of the development of the Coq proof assistant, I have created and maintained a multi-function bot to assist developers in automating some basic and repetitive tasks. In this talk, I will present a recent pull request that was submitted to the bot repository and this will be an opportunity to present the way the bot is architectured, and how it uses a modern, typed, GitHub API and suitable OCaml libraries to implement its features, and how that makes it easy to extend.

Cet exposé sera une introduction à l'algèbre linéaire graphique (graphical linear algebra), un langage qui permet de raisonner de façon compositionnelle à propos de système R-linéaires, pour divers semi-anneaux R. Lorsque que R est un corps, sa sémantique et sa théorie équationnelle sont bien comprises. Dans ce contexte, l'algèbre linéaire graphique est proche des signal flow graphs, un autre langage communément utilisé en théorie du contrôle pour spécifier des systèmes dynamiques au comportement linéaire. Des travaux récents ont montrés que, pour R = ℕ, la même syntaxe graphique permet de spécifier des systèmes concurrents qui manipulent des ressources discrètes. On obtient alors un langage suffisamment expressif pour y encoder très naturellement tous les réseaux de Petri et raisonner de façon modulaire à propos de leur comportement. Nous donnerons des axiomatisations complètes pour ces différentes interprétations et étudierons leurs extensions affines.

Il s'agit de travaux en collaboration avec Filippo Bonchi, Pawel Sobocinski et Fabio Zanasi.

The idea of Probabilistic Programming is to use the expressiveness of programming languages to build probabilistic models. To implement this idea, a common approach is to take a general purpose language and extend it with (1) a function that allows to sample a value from a distribution, (2) a function that allows to condition values of variables in a program via observations, and (3) an inference procedure that build a distribution for a program using the two previous constructs.

Following this approach, we propose to extends a reactive programming language with probabilistic constructs. This new language enables the modeling of probabilistic reactive systems, that is, probabilistic models in constant interaction with their environment. Examples of such systems include time-series prediction, agent-based systems, or infrastructure self-tuning.

To demonstrate this approach, we started from ReactiveML, a reactive extension of OCaml that supports parallel composition of processes, communication through signals, preemption, and suspension. We extend the language with classic probabilistic constructs (sample, factor à la WebPPL) and propose an inference scheme for reactive processes, that are, non-terminating functions.

Modern computing systems have grown in complexity, and the attack surface has increased accordingly.

Even though system components are generally carefully designed and even verified by different groups of people, the \textit{composition} of these components is often regarded with less attention.

This paves the way for “architectural attacks”, a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its component continues to act as expected.

In this article, we introduce FreeSpec, a Coq framework built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components.

FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition.

In doing so, we propose a novel approach for the Coq proof assistant to reason about programs with effects in a modular way.

Classical results from algebra, such as Hilbert's Basis Theorem and Hilbert’s Nullstellensatz, have been used to decide equivalence for some classes of transducers, such as HDT0L (Honkala 2000) or more recently deterministic tree-to-string transducers (Seidl, Maneth, Kemper 2015). In this talk, we propose an abstraction of these methods. The goal is to investigate the scope of the “Hilbert method” for transducer equivalence that was described above.

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

-We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.

-We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

This is an informal whiteboard/blackboard presentation on generative adversarial networks by a non-expert. I will explain integral probability metrics and their use on training deep generative models, widely known as GAN (generative adversarial networks). My plan is to focus on two well-known metrics for probability distributions, Wasserstein distance and Maximum Mean Discrepancy. I will explain how their dual characterisations have been used in the adversarial training of deep generative models, and I will make superficial/speculative comparisons between these metrics. My talk will be based on the following papers and the slides:

References: Wasserstein GAN https://arxiv.org/abs/1701.07875

Generative Models and Model Criticism via Optimized Maximum Mean Discrepancy https://arxiv.org/abs/1611.04488

Maximum Mean Discrepancy http://alex.smola.org/teaching/iconip2006/iconip_3.pdf

In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Reporting on joint work with V. Danos and I. Garnier, I will present a novel formulation of graph rewriting that permits to phrase the concept in a fashion akin to statistical physics. The key ingredient of this approach is the rule algebra framework, in which rewriting rules are interpreted as a type of diagrams endowed with a notion of sequential compositions. The focus of this talk will be the stochastic mechanics applications: once an associative algebra of rewriting rules is available in the form of the rule algebras, the full theory of continuous time Markov chains is at ones disposal. A number of explicit examples for computing in this formalism will be presented.

The usual epistemic S5 model for multi-agent systems is a Kripke graph, whose edges are labeled with the agents that do not distinguish between two states. We propose to uncover the higher dimensional information implicit in the Kripke graph, by using as a model its dual, a chromatic simplicial complex. For each state of the Kripke model there is a facet in the complex, with one vertex per agent. If an edge (u,v) is labeled with a set of agents S, the facets corresponding to u and v intersect in a simplex consisting of one vertex for each agent of S. Then we use dynamic epistemic logic to study how the simplicial complex epistemic model changes after the agents communicate with each other. We show that there are topological invariants preserved from the initial epistemic complex to the epistemic complex after an action model is applied, that depend on how reliable the communication is. In turn these topological properties determine the knowledge that the agents may gain after the communication happens.

We choose distributed computing as a case study to work out in detail the dynamic epistemic simplicial complex theory. The reason is that distributed computability has been studied using combinatorial topology, where the set of all possible executions in a distributed system is represented by a simplicial complex. We establish a formal, categorical equivalence between Kripke models and simplicial complex epistemic models.

In one direction, the connection provides a dynamic epistemic logic semantics to distributed computability, opening the possibility of reasoning about knowledge change in distributed computing. In the other direction, the connection allows to bring in the topological invariants known in distributed computing, to dynamic epistemic logic, and in particular show that knowledge gained after an epistemic action model is intimately related to higher dimensional topological properties.

Typestate-oriented programming is an extension of the OO paradigm in which objects are modelled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object’s internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. In this talk we examine a “full stack development”: we skip through a process calculus of actors equipped with a behavioural type system that allows to declare, to statically check and to infer state-based protocols, and we see it in action on Scala Akka programs, showing how far the standard Scala compiler supports protocol checking and discussing current work on compiler extension.

The client Must preorder relates tests (clients) instead of processes (servers). The existing characterisation of this preorder is unsatisfactory for it relies on the notion of usable clients which, in turn, are defined using an existential quantification over the servers that ensure client satisfaction. In this talk we characterise the set of usable clients for finite-branching LTSs, and give a sound and complete decision procedure for it. We also provide a novel coinductive characterisation of the client preorder, which we use to argue that the preorder is decidable, thus proving a claim made by Bernardi and Hennessy in 2013.

After decades of work on functional programming and on interactive theorem proving, a Haskell programmer who wants to include simple equational proofs in his programs, e.g. that some Monad laws hold, is still most likely to simply do the derivation as comments in the file, as all the advanced powerful proving tools are inconvenient.

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this rather hands-on talk I will show a small GHC plugin that I can use to prove the monad laws for a non-trivial functor. I am looking forward to a discussion of the merits, limits and capabilities of this approach.

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In the first part of the talk, I will first present an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and a sound characterisation of a subset of safe CFSMs from which global graphs can be constructed. In the second part, I will outline a few recent applications of this work to communicating timed automata and the Go programming language.

Les modèles d’interactions Booléens ont été introduits dans le contexte des réseaux de gènes par S. Kauffman dans la fin des années 60. On considère ici une variante, les modèles logiques, qui reposent sur un formalisme qualitatif avec mise à jour asynchrone des systèmes dynamiques discrets associés (R. Thomas, 1973). L’expression d'un gène y est représentée par une variable discrète et l’évolution du réseau est contrôlée par un système d'équations logiques. A partir de ce système peut être extrait un graphe de régulation : il s’agit d’un graphe orienté signé, dont les noeuds représentent les gènes, et les arcs les régulations entre gènes. On y distingue deux types de régulations : les activations (interactions positives) et les inhibitions (interactions négatives). Ces modèles génèrent des dynamiques de taille exponentielle, et nous faisons face à des problèmes d’explosion combinatoire. Ainsi, nous cherchons à caractériser des propriétés de la dynamique (attracteurs, atteignabilité,…) sans avoir à générer le graphe de transition d’états, qui représente l’ensemble des trajectoires possibles. Une méthode consiste à réduire le graphe, et étudier la dynamique réduite. L’opération de réduction crée des modifications potentiellement importantes dans la dynamique, il est donc nécessaire de bien caractériser ses propriétés de (non-)conservation. Nous verrons aussi comment identifier les attracteurs et quantifier leurs bassins d’attraction à l’aide de méthodes de Monte-Carlo adaptées. Enfin, nous mettrons en valeur ces méthodes d'analyse à travers l’étude d’un modèle concernant la tumorigénèse du cancer de vessie.

This talk describes a recently started ANR project named Colis (http://colis.irif.univ-paris-diderot.fr/), which has the goal of developing techniques and tools for the formal verification of shell scripts. More specifically, our goal is to verify the transformation of a file system tree described by so-called debian maintainer scripts. These scripts, often written in the Posix shell language, are part of the software packages in the Debian GNU/Linux distribution.

A possible example of a program specification is absence of execution error under certain initial conditions. Automatic program verification even for this kind of specification is a challenging task. In case of Debian maintainer scripts we are faced with even more challenging properties like idempotency of scripts (required by policy), or commutation of scripts.

The project is still in the beginning, so there are no results yet to present. However, I will explain why I think that the case of Debian maintainer scripts is very interesting for program verification : some aspects of scripts (POSIX shell, manipulation of a complex data structure) make the problem very difficult, while other aspects of the Debian case are likely to make the problem easier than the task of verifying any arbitary shell script.

The talk presents recent results on how to solve the general problem of computing the time evolution of means and moments of ``occurence counts in rule-based models; computability is in the sense of Weihrauch. Roughly, established techniques, namely adaptive uniformization and finite state projection, can be reused – provided that occurrence counts (and their powers) are bounded by a polynomial in the ``size of the rule-based system and the ``size'' of the system does not explode. The most interesting results can be obtained for context-free systems, which can be thought of as branching processes equipped with structure; for these systems we have PTIME computability.

All results will be exemplified for the case of string rewriting, aiming for a widest possible audience of computer scientists, assuming only basic knowledge of continous time Markov chains with countable state space. Computing the time evolution of mean word counts in stochastic string rewriting is already highly non-trivial, even if it is the most basic example. The GEM OF THE TALK is the computation of mean word counts for context-free grammars!