We present a framework for the formal modeling of state-based systems in the context of the Lean4 programming language and proof assistant. In this context, the main objective is to support a step-wise refinement methodology inspired conceptually by the Event-B formal method. As a starting point, the LeanMachines framework proposes Lean4 constructions for the main Event-B concepts such as contexts, machines and events. Most importantly, the associated refinement principles are introduced in the form of typeclass constructions inspired by (and in fact built upon) the Mathlib mathematical framework. Beyond the basic concepts and structures, we also experiment with extensions of the framework. First, we develop an algebra of event combinators that allow to compose complex event structures out of simpler ones. These combinators are based on algebraic structures—functors, arrows, and so on—that have been developed and studied in the context of (functional) programming language theory. Our proposed formalization of the Event-B concepts is very shallow in the sense that all the constructions are directly based on the Lean4 logic and abstractions. One benefit is that proof obligations can be discharged using the tactic language of Lean4 with almost no embedding overhead such as an abstraction barrier that would require syntactic conversions, or the necessity to use some dedicated proof tactics. As an important design guideline, we enforce the fundamental principle of correctness-by-construction: machine states, events structures and refinement steps cannot be fully constructed without discharging the prescribed proof obligations.

A deep connection exists between the interleaving semantics of concurrent processes and increasingly labelled combinatorial structures. In this paper we further explore this connection by studying the rich combinatorics of partially increasing structures underlying the operator of non-deterministic choice. Following the symbolic method of analytic combinatorics, we study the size of the computation trees induced by typical non-deterministic processes, providing a precise quantitative measure of the so-called "combinatorial explosion" phenomenon. Alternatively, we can see non-deterministic choice as encoding a family of tree-like partial orders. Measuring the (rather large) size of this family on average offers a key witness to the expressiveness of the choice operator. As a practical outcome of our quantitative study, we describe an efficient algorithm for generating computation paths uniformly at random.

We present a Petri net interpretation of the pi-graphs - a graphical variant of the picalculus where recursion and replication are replaced by iteration. The concise and syntax-driven translation can be used to reason in Petri net terms about open re

The Pi-calculus is a formalism to model and reason about highly concurrent and dynamic systems. Most of the expressive power of the language comes from the ability to pass communication channels among concurrent processes, as any other value. We present in this paper the CubeVM, an interpreter architecture for an applied variant of the Pi-calculus, focusing on its operational semantics. The main characteristic of the CubeVM comes from its stackless architecture. We show, in a formal way, that the resource management model inside the VM may be greatly simplified without the need for nested stack frames. This is particularly true for the garbage collection of processes and channels. The proposed GC, based on a reference counting scheme, is highly concurrent and, most interestingly, does automatically detect and reclaim cycles of disabled processes. We also address the main performance issues raised by the fine-grained concurrency model of the Pi-calculus. We introduce the reactive variant of the semantics that allows, when applicable, to increase the performance drastically by bypassing the scheduler. We define the language subset of processes in so called chain-reaction forms for which the sequential semantics can be proved statically. We illustrate the expressive power and performance gains of such chain-reactions with examples of functional, dataflow and object-oriented systems. Encodings for the pure Pi-calculus are also demonstrated.