From 5a73c8b29d2df3313a677450bc8bc096978932e5 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Thu, 16 Jul 2026 19:05:35 +0200
Subject: [PATCH 1/7] sp begins

---
 Cslib/Languages/StatefulProcesses/Basic.lean  | 138 ++++++++++++++++++
 .../Languages/StatefulProcesses/Network.lean  |  44 ++++++
 2 files changed, 182 insertions(+)
 create mode 100644 Cslib/Languages/StatefulProcesses/Basic.lean
 create mode 100644 Cslib/Languages/StatefulProcesses/Network.lean

diff --git a/Cslib/Languages/StatefulProcesses/Basic.lean b/Cslib/Languages/StatefulProcesses/Basic.lean
new file mode 100644
index 000000000..89904e0e7
--- /dev/null
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Semantics.LTS.Basic
+
+/-!
+# Stateful Processes
+
+The language of Stateful Processes (SP for short), a process calculus
+where processes communicate via message passing [Montesi2023]. Stateful processes or similar
+languages are typically used to model implementations of choreographic programs, but they can also
+be used as abstract representations that can be later compiled to executable mainstream languages.
+
+## Limitations
+
+The current formalisation does not cover process polymorphism (procedures do not take process
+parameters) nor general recursion (this is the tail-recursive fragment of Stateful Processes)
+
+## Implementation notes
+
+This development faithfully follows the presentation in [Montesi2023] but for a minor difference:
+we adopt a more structural approach to the operational semantics of the calculus, by defining
+a semantics of observable actions for processes.
+
+## References
+
+* [F. Montesi, *Introduction to Choreographies*][Montesi2023]
+-/
+
+@[expose] public section
+
+namespace Cslib.StatefulProcesses
+
+section Syntax
+
+/-! ## Syntax of process terms -/
+
+/-- Prefixes. -/
+inductive Process.Prefix (Pid Var Expr SelLabel : Type*) where
+  /-- Assign to `x` the result of evaluating `e`. -/
+  | assign (x : Var) (e : Expr)
+  /-- Send to `p` the result of evaluating `e`. -/
+  | sendValue (p : Pid) (e : Expr)
+  /-- Receive a value from `p` and store it in `x`. -/
+  | recvValue (p : Pid) (x : Var)
+  /-- Send to `p` the label `l`. -/
+  | sendLabel (p : Pid) (l : SelLabel)
+deriving DecidableEq
+
+/-- Processes. -/
+inductive Process (Pid Var Expr SelLabel ProcName : Type*) where
+  /-- The terminated process. -/
+  | nil
+  /-- Execute the prefix `prf` and proceed as the continuation `pr`. -/
+  | pre (prf : Process.Prefix Pid Var Expr SelLabel) (pr : Process Pid Var Expr SelLabel ProcName)
+  /-- Branching process: receives a selection label and continues accordingly. -/
+  | recvLabel (p : Pid) (branches : List (SelLabel × Process Pid Var Expr SelLabel ProcName))
+  /-- Conditional: evaluate `e` to choose between `pr₁` and `pr₂`. -/
+  | cond (e : Expr) (pr₁ pr₂ : Process Pid Var Expr SelLabel ProcName)
+  /-- Call the procedure `proc`. -/
+  | call (proc : ProcName) (ps : List Pid)
+
+instance : Zero (Process Pid Var Expr SelLabel ProcName) := ⟨.nil⟩
+
+declare_syntax_cat pre
+scoped syntax term "≔" term : pre
+scoped syntax term "!" term : pre
+scoped syntax term "?" term : pre
+scoped syntax term "⊕" term : pre
+scoped syntax "[SPpre|" pre "]" : term
+scoped macro "[SPpre|" x:term "≔" e:term "]" : term => `(Process.Prefix.assign $x $e)
+scoped macro "[SPpre|" p:term "!" e:term "]" : term => `(Process.Prefix.sendValue $p $e)
+scoped macro "[SPpre|" p:term "?" x:term "]" : term => `(Process.Prefix.recvValue $p $x)
+scoped macro "[SPpre|" p:term "⊕" l:term "]" : term => `(Process.Prefix.sendLabel $p $l)
+
+declare_syntax_cat proc
+scoped syntax num : proc
+scoped syntax pre : proc
+scoped syntax pre "; " proc : proc
+scoped syntax "if" term "then" proc "else" proc : proc
+scoped syntax "[SP|" proc "]" : term
+scoped macro_rules
+  | `([SP|0]) => `(0)
+  | `([SP|$prf:pre; $pr:proc]) => `(Process.pre `([SPpre|$prf]) `([SP|$pr]))
+  | `([SP|$prf:pre]) => `(Process.pre `([SPpre|$prf]) 0)
+  | `([SP|if $e then $p₁:proc else $p₂:proc]) => `(Process.cond $e `([SP|$p₁]) `([SP|$p₂]))
+
+end Syntax
+
+section Semantics
+
+/-! ## Semantics -/
+
+/-- Actions. -/
+inductive Act (Pid Var Expr SelLabel : Type*) where
+  /-- Assign to `x` the result of evaluating `e`. -/
+  | assign (x : Var) (e : Expr)
+  /-- Send to `p` the result of evaluating `e`. -/
+  | sendValue (p : Pid) (e : Expr)
+  /-- Receive a value from `p` and store it in variable `x`. -/
+  | recvValue (p : Pid) (x : Var)
+  /-- Send to `p` the selection label `l`. -/
+  | sendLabel (p : Pid) (l : SelLabel)
+  /-- Receive from `p` the selection label `l`. -/
+  | recvLabel (p : Pid) (l : SelLabel)
+  /-- Choose the then-branch of a conditional guarded by `e`. -/
+  | condThen (e : Expr)
+  /-- Choose the else-branch of a conditional guarded by `e`. -/
+  | condElse (e : Expr)
+deriving DecidableEq
+
+abbrev Process.Prefix.toAct : Process.Prefix Pid Var Expr SelLabel → Act Pid Var Expr SelLabel
+  | assign x e => .assign x e
+  | sendValue p e => .sendValue p e
+  | recvValue p x => .recvValue p x
+  | sendLabel p l => .sendLabel p l
+
+/-- Transition relation for processes.
+Do not use this directly, use `Process.lts` instead. -/
+inductive Process.Tr :
+    Process Pid Var Expr SelLabel ProcName → Act Pid Var Expr SelLabel →
+    Process Pid Var Expr SelLabel ProcName → Prop
+  | pre : Tr (pre prf pr) prf.toAct (pr)
+  | condThen : Tr (cond e pr₁ pr₂) (.condThen e) pr₁
+  | condElse : Tr (cond e pr₁ pr₂) (.condElse e) pr₂
+  | recvLabel (h : (l, pr) ∈ branches): Tr (recvLabel p branches) (.recvLabel p l) pr
+
+def Process.lts :
+    LTS (Process Pid Var Expr SelLabel ProcName) (Act Pid Var Expr SelLabel) := ⟨Process.Tr⟩
+
+end Semantics
+
+end Cslib.StatefulProcesses
diff --git a/Cslib/Languages/StatefulProcesses/Network.lean b/Cslib/Languages/StatefulProcesses/Network.lean
new file mode 100644
index 000000000..e996926d6
--- /dev/null
+++ b/Cslib/Languages/StatefulProcesses/Network.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Languages.StatefulProcesses.Basic
+public import Cslib.Foundations.Data.FinFun.Basic
+
+/-! # Semantics of stateful process networks
+
+## Implementation notes
+
+We leverage the fact that networks are functions to formulate the semantics without requiring a
+definition of parallel composition.
+
+## References
+
+* [F. Montesi, *Introduction to Choreographies*][Montesi2023]
+-/
+
+@[expose] public section
+
+namespace Cslib.StatefulProcesses
+
+open scoped FinFun
+
+/-- A network maps process names to process terms. -/
+abbrev Network (Pid Var Expr SelLabel ProcName : Type*) :=
+  Pid → Process Pid Var Expr SelLabel ProcName
+
+namespace Network
+
+inductive TrLabel Pid Var Expr SelLabel ProcName : Network
+
+def lts :
+    LTS (Network Pid Var Expr SelLabel ProcName) (Pid × Act Pid Var Expr SelLabel) :=
+
+
+end Network
+
+end Cslib.StatefulProcesses

From bae0bf6a27c6f130ee48f76832fcf8755a1770d0 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 22 Jul 2026 13:30:15 +0200
Subject: [PATCH 2/7] mech begins

---
 Cslib/Foundations/Syntax/HasSubstitution.lean |   7 +
 Cslib/Languages/Mech/README.md                |  40 +++++
 Cslib/Languages/README.md                     |   1 +
 Cslib/Languages/StatefulProcesses/Basic.lean  | 131 +++++++++------
 .../Languages/StatefulProcesses/Network.lean  | 149 ++++++++++++++++--
 CslibTests/StatefulProcesses.lean             |  74 +++++++++
 references.bib                                |   3 +
 7 files changed, 342 insertions(+), 63 deletions(-)
 create mode 100644 Cslib/Languages/Mech/README.md
 create mode 100644 CslibTests/StatefulProcesses.lean

diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean
index b9b31470b..ae69bf6cd 100644
--- a/Cslib/Foundations/Syntax/HasSubstitution.lean
+++ b/Cslib/Foundations/Syntax/HasSubstitution.lean
@@ -38,4 +38,11 @@ meta def unexpandHasSubstitutionSubst : Lean.PrettyPrinter.Unexpander
   | `($_ $t $x $s) => `($t[$x := $s])
   | _ => throw ()
 
+namespace HasSubstitution
+
+instance [DecidableEq α] : HasSubstitution (α → β) α β where
+  subst := Function.update
+
+end HasSubstitution
+
 end Cslib
diff --git a/Cslib/Languages/Mech/README.md b/Cslib/Languages/Mech/README.md
new file mode 100644
index 000000000..056db87d1
--- /dev/null
+++ b/Cslib/Languages/Mech/README.md
@@ -0,0 +1,40 @@
+<pre>
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+</pre>
+
+# Mech: Mechanised Choreographic Programming
+
+This directory is a placeholder for the upstreaming of Mech, a language for choreographic programming developed at FORM.
+
+Mech is a verified choreographic programming framework. It can be used to:
+1. Codify distributed protocols and systems in a choreographic language, benefitting from the simple global view of the 'Alice and Bob' protocol notation.
+2. Reason about choreographic programs with CSLib's foundations and tools
+3. Compile choreographies into provably-correct models of distributed programs in a process calculus.
+
+
+## Principles and plans
+
+### Protocol library development
+
+We plan on using Mech to develop a library of verified protocol for concurrent and distributed systems.
+
+### Support CSLib's compilation infrastructure
+
+Mech is sufficiently complex to test CSLib's infrastructure for compiler verification. We will establish a strong bisimilarity for the choreography compiler, enabling the transference of results from choreographies to their compiled versions.
+
+### Iterative approach
+
+A downstream version of Mech already exists at FORM -- CSLib originally started as a spin-off of some general components developed to make Mech possible, like `LTS`. This version is fairly complete, as it formalises most of the textbook theory of choreographic programming ('Introduction to Choreographies'), but some parts require adaptation or generalisation to be included in CSLib.
+
+We follow an iterative approach, whereby we introduce core components and then gradually augment them with more advanced features (like recursion, nondeterminism, etc.).
+
+### Placement
+
+Components that might be of interest beyond Mech (like [StatefulProcesses](../StatefulProcesses), a calculus used in some variation over different research papers) are placed outside of this directory.
+
+### Ergonomics
+
+- The current development has many unbundled parameters (for types, local computation, etc.). We plan on exploring convenient bundled interfaces for easier use. See also the [tests for StatefulProcesses](/CslibTests/StatefulProcesses.lean).
+- We could use a lot more convenience in escaping to Lean for expression evaluation. This is nontrivial because we need to resolve variables from the local store of the appropriate process.
\ No newline at end of file
diff --git a/Cslib/Languages/README.md b/Cslib/Languages/README.md
index eb6722ccd..17fbd53e1 100644
--- a/Cslib/Languages/README.md
+++ b/Cslib/Languages/README.md
@@ -1,6 +1,7 @@
 <pre>
 Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
 </pre>
 
 # Languages
diff --git a/Cslib/Languages/StatefulProcesses/Basic.lean b/Cslib/Languages/StatefulProcesses/Basic.lean
index 89904e0e7..dda77065c 100644
--- a/Cslib/Languages/StatefulProcesses/Basic.lean
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -8,27 +8,33 @@ module
 
 public import Cslib.Foundations.Semantics.LTS.Basic
 
+set_option linter.style.longLine false in
 /-!
 # Stateful Processes
 
 The language of Stateful Processes (SP for short), a process calculus
 where processes communicate via message passing [Montesi2023]. Stateful processes or similar
-languages are typically used to model implementations of choreographic programs, but they can also
-be used as abstract representations that can be later compiled to executable mainstream languages.
+languages are typically used to model implementations of choreographic programs (concurrent and/or
+distributed protocols), but they are also designed to be used as abstract representations that can
+be later compiled to executable mainstream languages.
 
 ## Limitations
 
 The current formalisation does not cover process polymorphism (procedures do not take process
-parameters) nor general recursion (this is the tail-recursive fragment of Stateful Processes)
+parameters) nor general recursion (this is the tail-recursive fragment of Stateful Processes).
+For recursion, only the syntax is currently implemented. Its semantics will follow a similar
+approach to that for `CCS`.
 
 ## Implementation notes
 
-This development faithfully follows the presentation in [Montesi2023] but for a minor difference:
-we adopt a more structural approach to the operational semantics of the calculus, by defining
-a semantics of observable actions for processes.
+This development follows the presentation in [Montesi2023], with one difference: we adopt a modular
+approach to the definition of operational semantics, by first defining a symbolic semantics from
+which a concrete semantics is then derived by adding stores (process memory). This approach is
+described in [Acclavio2026].
 
 ## References
 
+* [M. Acclavio, G. Manara, F. Montesi, X. Qin, *Choreographic Programming: a Semantic Approach*][Acclavio2026]
 * [F. Montesi, *Introduction to Choreographies*][Montesi2023]
 -/
 
@@ -40,55 +46,77 @@ section Syntax
 
 /-! ## Syntax of process terms -/
 
+/-- Expressions for local computation. -/
+inductive Expr (Var Val FunId : Type*) where
+  /-- Read variable `x`. -/
+  | var (x : Var)
+  /-- Value `v`. -/
+  | val (v : Val)
+  /-- Call function `f` with arguments `args`. -/
+  | call (f : FunId) (args : List (Expr Var Val FunId))
+
+/-- Utility instance to write variables directly as expressions. -/
+instance : Coe Var (Expr Var Val FunId) where
+  coe x := .var x
+
+/-- Utility instance to write values directly as expressions. -/
+instance : Coe Val (Expr Var Val FunId) where
+  coe v := .val v
+
 /-- Prefixes. -/
-inductive Process.Prefix (Pid Var Expr SelLabel : Type*) where
+inductive Prefix (Pid Var Val FunId SelLabel : Type*) where
   /-- Assign to `x` the result of evaluating `e`. -/
-  | assign (x : Var) (e : Expr)
+  | assign (x : Var) (e : Expr Var Val FunId)
   /-- Send to `p` the result of evaluating `e`. -/
-  | sendValue (p : Pid) (e : Expr)
+  | sendValue (p : Pid) (e : Expr Var Val FunId)
   /-- Receive a value from `p` and store it in `x`. -/
   | recvValue (p : Pid) (x : Var)
   /-- Send to `p` the label `l`. -/
   | sendLabel (p : Pid) (l : SelLabel)
-deriving DecidableEq
 
 /-- Processes. -/
-inductive Process (Pid Var Expr SelLabel ProcName : Type*) where
+inductive Process (Pid Var Val FunId SelLabel ProcName : Type*) where
   /-- The terminated process. -/
   | nil
   /-- Execute the prefix `prf` and proceed as the continuation `pr`. -/
-  | pre (prf : Process.Prefix Pid Var Expr SelLabel) (pr : Process Pid Var Expr SelLabel ProcName)
+  | pre (prf : Prefix Pid Var Val FunId SelLabel) (pr : Process Pid Var Val FunId SelLabel ProcName)
   /-- Branching process: receives a selection label and continues accordingly. -/
-  | recvLabel (p : Pid) (branches : List (SelLabel × Process Pid Var Expr SelLabel ProcName))
+  | recvLabel (p : Pid) (branches : List (SelLabel × Process Pid Var Val FunId SelLabel ProcName))
   /-- Conditional: evaluate `e` to choose between `pr₁` and `pr₂`. -/
-  | cond (e : Expr) (pr₁ pr₂ : Process Pid Var Expr SelLabel ProcName)
+  | cond (e : Expr Var Val FunId) (pr₁ pr₂ : Process Pid Var Val FunId SelLabel ProcName)
   /-- Call the procedure `proc`. -/
   | call (proc : ProcName) (ps : List Pid)
 
-instance : Zero (Process Pid Var Expr SelLabel ProcName) := ⟨.nil⟩
-
-declare_syntax_cat pre
-scoped syntax term "≔" term : pre
-scoped syntax term "!" term : pre
-scoped syntax term "?" term : pre
-scoped syntax term "⊕" term : pre
-scoped syntax "[SPpre|" pre "]" : term
-scoped macro "[SPpre|" x:term "≔" e:term "]" : term => `(Process.Prefix.assign $x $e)
-scoped macro "[SPpre|" p:term "!" e:term "]" : term => `(Process.Prefix.sendValue $p $e)
-scoped macro "[SPpre|" p:term "?" x:term "]" : term => `(Process.Prefix.recvValue $p $x)
-scoped macro "[SPpre|" p:term "⊕" l:term "]" : term => `(Process.Prefix.sendLabel $p $l)
-
-declare_syntax_cat proc
-scoped syntax num : proc
-scoped syntax pre : proc
-scoped syntax pre "; " proc : proc
-scoped syntax "if" term "then" proc "else" proc : proc
-scoped syntax "[SP|" proc "]" : term
+instance : Zero (Process Pid Var Val FunId SelLabel ProcName) := ⟨.nil⟩
+
+declare_syntax_cat sp_pre
+scoped syntax term:max "≔" term : sp_pre
+scoped syntax term:max "!" term : sp_pre
+scoped syntax term:max "?" term : sp_pre
+scoped syntax term:max "⊕" term : sp_pre
+scoped syntax "`(SPpre|" sp_pre ")" : term
+
+scoped macro_rules
+  | `(`(SPpre| $x:term ≔ $e:term )) => `(Prefix.assign $x $e)
+  | `(`(SPpre| $p:term ! $e:term )) => `(Prefix.sendValue $p $e)
+  | `(`(SPpre| $p:term ? $x:term )) => `(Prefix.recvValue $p $x)
+  | `(`(SPpre| $p:term ⊕ $l:term )) => `(Prefix.sendLabel $p $l)
+
+declare_syntax_cat sp_proc
+scoped syntax num : sp_proc
+scoped syntax sp_pre "; " sp_proc : sp_proc
+scoped syntax term:max "&" term : sp_proc
+scoped syntax "if" term "then" sp_proc "else" sp_proc : sp_proc
+-- The next syntax would be nice to have to avoid having trailing 0s in examples.
+-- scoped syntax:min "`(SP| " sp_pre ")" : term
+scoped syntax "`(SP| " sp_proc ")" : term
 scoped macro_rules
-  | `([SP|0]) => `(0)
-  | `([SP|$prf:pre; $pr:proc]) => `(Process.pre `([SPpre|$prf]) `([SP|$pr]))
-  | `([SP|$prf:pre]) => `(Process.pre `([SPpre|$prf]) 0)
-  | `([SP|if $e then $p₁:proc else $p₂:proc]) => `(Process.cond $e `([SP|$p₁]) `([SP|$p₂]))
+  | `(`(SP| 0)) => `(0)
+  | `(`(SP| $prf:sp_pre; $pr:sp_proc)) => `(Process.pre `(SPpre| $prf) `(SP| $pr))
+  -- | `(`(SP| $prf:sp_pre)) => `(Process.pre `(SPpre| $prf) 0)
+  | `(`(SP| $p:term & $l:term)) => `(Process.recvLabel $p $l)
+  | `(`(SP| if $e:term then $p₁:sp_proc else $p₂:sp_proc)) =>
+    `(Process.cond $e `(SP| $p₁) `(SP| $p₂))
 
 end Syntax
 
@@ -97,11 +125,11 @@ section Semantics
 /-! ## Semantics -/
 
 /-- Actions. -/
-inductive Act (Pid Var Expr SelLabel : Type*) where
+inductive Act (Pid Var Val FunId SelLabel : Type*) where
   /-- Assign to `x` the result of evaluating `e`. -/
-  | assign (x : Var) (e : Expr)
+  | assign (x : Var) (e : Expr Var Val FunId)
   /-- Send to `p` the result of evaluating `e`. -/
-  | sendValue (p : Pid) (e : Expr)
+  | sendValue (p : Pid) (e : Expr Var Val FunId)
   /-- Receive a value from `p` and store it in variable `x`. -/
   | recvValue (p : Pid) (x : Var)
   /-- Send to `p` the selection label `l`. -/
@@ -109,29 +137,36 @@ inductive Act (Pid Var Expr SelLabel : Type*) where
   /-- Receive from `p` the selection label `l`. -/
   | recvLabel (p : Pid) (l : SelLabel)
   /-- Choose the then-branch of a conditional guarded by `e`. -/
-  | condThen (e : Expr)
+  | condThen (e : Expr Var Val FunId)
   /-- Choose the else-branch of a conditional guarded by `e`. -/
-  | condElse (e : Expr)
-deriving DecidableEq
+  | condElse (e : Expr Var Val FunId)
+
+/-- An action is internal if it is not meant to interact with another process. -/
+def Act.isInternal : Act Pid Var Val FunId SelLabel → Bool
+  | assign _ _ | condThen _ | condElse _ => true
+  | _ => false
 
-abbrev Process.Prefix.toAct : Process.Prefix Pid Var Expr SelLabel → Act Pid Var Expr SelLabel
+/-- Transforms a `Prefix` into an `Act`. -/
+abbrev Prefix.toAct : Prefix Pid Var Val FunId SelLabel → Act Pid Var Val FunId SelLabel
   | assign x e => .assign x e
   | sendValue p e => .sendValue p e
   | recvValue p x => .recvValue p x
   | sendLabel p l => .sendLabel p l
 
-/-- Transition relation for processes.
+/-- Symbolic transition relation for processes.
 Do not use this directly, use `Process.lts` instead. -/
 inductive Process.Tr :
-    Process Pid Var Expr SelLabel ProcName → Act Pid Var Expr SelLabel →
-    Process Pid Var Expr SelLabel ProcName → Prop
+    Process Pid Var Val FunId SelLabel ProcName → Act Pid Var Val FunId SelLabel →
+    Process Pid Var Val FunId SelLabel ProcName → Prop
   | pre : Tr (pre prf pr) prf.toAct (pr)
   | condThen : Tr (cond e pr₁ pr₂) (.condThen e) pr₁
   | condElse : Tr (cond e pr₁ pr₂) (.condElse e) pr₂
   | recvLabel (h : (l, pr) ∈ branches): Tr (recvLabel p branches) (.recvLabel p l) pr
 
+/-- Symbolic LTS of processes. -/
 def Process.lts :
-    LTS (Process Pid Var Expr SelLabel ProcName) (Act Pid Var Expr SelLabel) := ⟨Process.Tr⟩
+    LTS (Process Pid Var Val FunId SelLabel ProcName) (Act Pid Var Val FunId SelLabel) :=
+  ⟨Process.Tr⟩
 
 end Semantics
 
diff --git a/Cslib/Languages/StatefulProcesses/Network.lean b/Cslib/Languages/StatefulProcesses/Network.lean
index e996926d6..4ed9d0ef2 100644
--- a/Cslib/Languages/StatefulProcesses/Network.lean
+++ b/Cslib/Languages/StatefulProcesses/Network.lean
@@ -7,9 +7,12 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Languages.StatefulProcesses.Basic
-public import Cslib.Foundations.Data.FinFun.Basic
+public import Cslib.Foundations.Syntax.HasSubstitution
 
-/-! # Semantics of stateful process networks
+/-! # Networks of stateful processes and their semantics
+
+This module defines networks (maps from process names to process terms), as well as their symbolic
+and concrete operational semantics.
 
 ## Implementation notes
 
@@ -25,20 +28,136 @@ definition of parallel composition.
 
 namespace Cslib.StatefulProcesses
 
-open scoped FinFun
+/-! ## Networks and their symbolic semantics -/
 
 /-- A network maps process names to process terms. -/
-abbrev Network (Pid Var Expr SelLabel ProcName : Type*) :=
-  Pid → Process Pid Var Expr SelLabel ProcName
-
-namespace Network
-
-inductive TrLabel Pid Var Expr SelLabel ProcName : Network
-
-def lts :
-    LTS (Network Pid Var Expr SelLabel ProcName) (Pid × Act Pid Var Expr SelLabel) :=
-
-
-end Network
+abbrev Network (Pid Var Val FunId SelLabel ProcName : Type*) :=
+  Pid → Process Pid Var Val FunId SelLabel ProcName
+
+/-- The 0 ('zero') network, mapping all processes to the process term 0. -/
+instance : Zero (Network Pid Var Val FunId SelLabel ProcName) := ⟨fun _ => 0⟩
+
+/-- Symbolic transition labels for networks. -/
+inductive Network.TrLabel Pid Var Val FunId SelLabel
+  | local (p : Pid) (μ : Act Pid Var Val FunId SelLabel)
+  | com (p : Pid) (e : Expr Var Val FunId) (q : Pid) (x : Var)
+  | sel (p : Pid) (q : Pid) (l : SelLabel)
+
+variable [DecidableEq Pid]
+
+/-- Symbolic transition relation for networks. -/
+inductive Network.Tr :
+    Network Pid Var Val FunId SelLabel ProcName → TrLabel Pid Var Val FunId SelLabel →
+    Network Pid Var Val FunId SelLabel ProcName → Prop
+  | local
+    (hμ : μ.isInternal) (htr : Process.lts.Tr (n p) μ prP)
+    (hn' : n' = n[p := prP]) :
+    Tr n (TrLabel.local p μ) n'
+  | com
+    (hsend : Process.lts.Tr (n p) (.sendValue q e) prP)
+    (hrecv : Process.lts.Tr (n q) (.recvValue p x) prQ)
+    (hn' : n' = n[p := prP][q := prQ]) :
+    Tr n (TrLabel.com p e q x) n'
+  | sel
+    (hsend : Process.lts.Tr (n p) (.sendLabel q l) prP)
+    (hrecv : Process.lts.Tr (n q) (.recvLabel p l) prQ)
+    (hn' : n' = n[p := prP][q := prQ]) :
+    Tr n (TrLabel.sel p q l) n'
+
+/-- Symbolic LTS of networks. -/
+def Network.lts :
+    LTS (Network Pid Var Val FunId SelLabel ProcName) (TrLabel Pid Var Val FunId SelLabel) :=
+  ⟨Network.Tr⟩
+
+/-! ## Stores, evaluation, and concrete semantics of networks -/
+
+/-- A local store represents the memory state of a process, mapping variables to values. -/
+abbrev LocalStore Var Val := (x : Var) → Val
+
+/-- Type of (potentially nondeterministic) evaluation relations for function calls. -/
+abbrev FunCallEval FunId Val := (f : FunId) → (args : List Val) → Val → Prop
+
+/-- Evaluation relation. -/
+inductive FunCallEval.EvalExpr (Eval : FunCallEval FunId Val) :
+    (σ : LocalStore Var Val) → (e : Expr Var Val FunId) → (v : Val) → Prop where
+  /-- A value evaluates to itself. -/
+  | val : Eval.EvalExpr σ (.val v) v
+  /-- A variable evaluates to its mapped value in the store. -/
+  | var : Eval.EvalExpr σ (.var x) (σ x)
+  /-- A function call first recursively evaluates its expression arguments, and then
+  invokes the parameter for function evaluation. -/
+  | call
+    (hArgs : List.Forall₂ (Eval.EvalExpr σ) args vals)
+    (hFun : Eval f vals v) :
+    Eval.EvalExpr σ (.call f args) v
+
+/-- A global store represents the memory state of an entire system, mapping each process to its
+local store. -/
+abbrev GlobalStore Pid Var Val := (p : Pid) → LocalStore Var Val
+
+/-- Configurations, consisting of a network and a global store. -/
+structure Cfg (Pid Var Val FunId SelLabel ProcName : Type*) where
+  net : Network Pid Var Val FunId SelLabel ProcName
+  store : GlobalStore Pid Var Val
+
+/-- Transition labels for network configurations.
+
+These labels model what can be observed from execution, and thus hide internal computational
+details.
+-/
+inductive Cfg.TrLabel Pid Val SelLabel
+  | local (p : Pid)
+  | com (p : Pid) (q : Pid) (v : Val)
+  | sel (p : Pid) (q : Pid) (l : SelLabel)
+
+/-- Type of an element of type `α` located at a process. -/
+abbrev AtPid Pid α := Pid × α
+
+/-- The process name of a located element. -/
+abbrev AtPid.pid (a : AtPid Pid α) := a.fst
+
+/-- The element of a located element. -/
+abbrev AtPid.elem (a : AtPid Pid α) := a.snd
+
+instance [DecidableEq Var] : HasSubstitution (GlobalStore Pid Var Val) (AtPid Pid Var) Val where
+  subst gs px v := gs[px.fst := ((gs px.pid)[px.elem := v])]
+
+/-- Transition relation for network configurations. -/
+inductive Cfg.Tr [DecidableEq Var] (isTrue : Val → Bool) (Eval : FunCallEval FunId Val) :
+    Cfg Pid Var Val FunId SelLabel ProcName → Cfg.TrLabel Pid Val SelLabel →
+    Cfg Pid Var Val FunId SelLabel ProcName → Prop where
+  -- Internal actions
+  | assign
+    (htr : Network.lts.Tr cfg.net (.local p (.assign x e)) cfg'.net)
+    (heval : Eval.EvalExpr (cfg.store p) e v)
+    (hstore : cfg'.store = cfg.store[(p, x) := v]) :
+    Tr isTrue Eval cfg (Cfg.TrLabel.local p) cfg'
+  | condThen
+    (htr : Network.lts.Tr cfg.net (.local p (.condThen e)) cfg'.net)
+    (heval : Eval.EvalExpr (cfg.store p) e v)
+    (hguard : isTrue v)
+    (hstore : cfg'.store = cfg.store) :
+    Tr isTrue Eval cfg (Cfg.TrLabel.local p) cfg'
+  | condElse
+    (htr : Network.lts.Tr cfg.net (.local p (.condElse e)) cfg'.net)
+    (heval : Eval.EvalExpr (cfg.store p) e v)
+    (hguard : ¬isTrue v)
+    (hstore : cfg'.store = cfg.store) :
+    Tr isTrue Eval cfg (Cfg.TrLabel.local p) cfg'
+  -- Interactions
+  | com
+    (htr : Network.lts.Tr cfg.net (.com p e q x) cfg'.net)
+    (heval : Eval.EvalExpr (cfg.store p) e v)
+    (hstore : cfg'.store = cfg.store[(q, x) := v]) :
+    Tr isTrue Eval cfg (Cfg.TrLabel.com p q v) cfg'
+  | sel
+    (htr : Network.lts.Tr cfg.net (.sel p q l) cfg'.net)
+    (hstore : cfg'.store = cfg.store) :
+    Tr isTrue Eval cfg (Cfg.TrLabel.sel p q l) cfg'
+
+/-- LTS of network configurations. -/
+def Cfg.lts [DecidableEq Var] (isTrue : Val → Bool) (Eval : FunCallEval FunId Val) :
+    LTS (Cfg Pid Var Val FunId SelLabel ProcName) (Cfg.TrLabel Pid Val SelLabel) :=
+  ⟨Cfg.Tr isTrue Eval⟩
 
 end Cslib.StatefulProcesses
diff --git a/CslibTests/StatefulProcesses.lean b/CslibTests/StatefulProcesses.lean
new file mode 100644
index 000000000..43fdf0fba
--- /dev/null
+++ b/CslibTests/StatefulProcesses.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Languages.StatefulProcesses.Basic
+import Cslib.Languages.StatefulProcesses.Network
+
+namespace CslibTests
+
+open Cslib.StatefulProcesses
+
+-- Notation
+
+example (x : Var) (e : Expr Var Val FunId) :
+    (`(SPpre|x ≔ e) : Prefix Pid Var Val FunId SelLabel) =
+    (Prefix.assign x e) := by
+  rfl
+
+example (x : Var) (e : Expr Var Val FunId) :
+    (`(SP|x ≔ e; 0) : Process Pid Var Val FunId SelLabel ProcName) =
+    Process.pre (Prefix.assign x e) 0 := by
+  rfl
+
+-- Semantics
+
+open Cslib
+open Cslib.StatefulProcesses.Network
+
+section Hello
+
+/-!
+A simple example where "p" sends the string `"Hello"` to "q".
+-/
+
+/-- A simple stringified process type. -/
+abbrev HelloProcess := Process String String String String String String
+
+/-- A simple stringified network type. -/
+abbrev HelloNetwork := Network String String String String String String
+
+def helloNet : HelloNetwork := fun p =>
+  if p = "p" then `(SP|"q"!"Hello"; 0)
+  else if p = "q" then `(SP|"p"?"x"; 0)
+  else 0
+
+/-- A simple stringified configuration type. -/
+abbrev HelloCfg := Cfg String String String String String String
+
+def helloCfg : HelloCfg where
+  net := helloNet
+  store := fun _ => fun _ => ""
+
+def stringIsTrue (s : String) := s == "true"
+
+/-- All functions evaluate to "⊥". -/
+def HelloEval : FunCallEval String String := fun _ _ v => v = "⊥"
+
+def helloLts : LTS HelloCfg (Cfg.TrLabel String String String) := Cfg.lts stringIsTrue HelloEval
+
+-- Example transition.
+-- This is begging for more automation.
+example : helloLts.Tr helloCfg (.com "p" "q" "Hello")
+    (Cfg.mk 0 (helloCfg.store[("q", "x") := "Hello"])) := by
+  apply Cfg.Tr.com (heval := by constructor) (hstore := rfl)
+  apply Network.Tr.com (by constructor) (by constructor)
+  ext p
+  simp only [Pi.zero_apply, helloCfg, HasSubstitution.subst]
+  grind [helloNet]
+
+end Hello
+
+end CslibTests
diff --git a/references.bib b/references.bib
index 18281428d..42aaff9eb 100644
--- a/references.bib
+++ b/references.bib
@@ -1,3 +1,6 @@
+@article{Acclavio2026,
+}
+
 @inproceedings{Aceto1999,
   author       = {Luca Aceto and
                   Anna Ing{\'{o}}lfsd{\'{o}}ttir},

From e3b959112f7972e3362ba64d7175b03c4bc77fa1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 29 Jul 2026 13:23:03 +0200
Subject: [PATCH 3/7] add missing citation

---
 references.bib | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/references.bib b/references.bib
index 3a1855d84..6af9dafc4 100644
--- a/references.bib
+++ b/references.bib
@@ -1,4 +1,11 @@
-@article{Acclavio2026,
+@misc{Acclavio2026,
+      title={Choreographic Programming: a Semantic Approach}, 
+      author={Matteo Acclavio and Giulia Manara and Fabrizio Montesi and Xueying Qin},
+      year={2026},
+      eprint={2607.23793},
+      archivePrefix={arXiv},
+      primaryClass={cs.PL},
+      url={https://arxiv.org/abs/2607.23793}, 
 }
 
 @inproceedings{Aceto1999,

From 1ee930509351b72382f66325fb1dff394d494162 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 29 Jul 2026 13:54:18 +0200
Subject: [PATCH 4/7] mk_all

---
 Cslib.lean      | 2 ++
 CslibTests.lean | 1 +
 2 files changed, 3 insertions(+)

diff --git a/Cslib.lean b/Cslib.lean
index 281dea9c2..97c085bd4 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -147,6 +147,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.StatefulProcesses.Basic
+public import Cslib.Languages.StatefulProcesses.Network
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.HML.LogicalEquivalence
 public import Cslib.Logics.LinearLogic.CLL.Basic
diff --git a/CslibTests.lean b/CslibTests.lean
index ed3063209..8bc051b31 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -14,3 +14,4 @@ import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Modal
 import CslibTests.Reduction
+import CslibTests.StatefulProcesses

From e5c6bb2df15199cc6d73be56f99e3e8e9c784ce2 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 29 Jul 2026 14:00:15 +0200
Subject: [PATCH 5/7] long line fix

---
 Cslib/Languages/StatefulProcesses/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Languages/StatefulProcesses/Basic.lean b/Cslib/Languages/StatefulProcesses/Basic.lean
index dda77065c..e6dd7d8df 100644
--- a/Cslib/Languages/StatefulProcesses/Basic.lean
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Semantics.LTS.Basic
 
+set_option linter.style.header false in
 set_option linter.style.longLine false in
 /-!
 # Stateful Processes

From bcddab51fa397bc283ba4813c27c2702dd48be88 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 29 Jul 2026 14:12:01 +0200
Subject: [PATCH 6/7] lint fixes

---
 Cslib/Languages/StatefulProcesses/Basic.lean  | 54 +++++++++++++------
 .../Languages/StatefulProcesses/Network.lean  |  2 +
 2 files changed, 40 insertions(+), 16 deletions(-)

diff --git a/Cslib/Languages/StatefulProcesses/Basic.lean b/Cslib/Languages/StatefulProcesses/Basic.lean
index e6dd7d8df..7ed463b9a 100644
--- a/Cslib/Languages/StatefulProcesses/Basic.lean
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -90,12 +90,22 @@ inductive Process (Pid Var Val FunId SelLabel ProcName : Type*) where
 
 instance : Zero (Process Pid Var Val FunId SelLabel ProcName) := ⟨.nil⟩
 
-declare_syntax_cat sp_pre
-scoped syntax term:max "≔" term : sp_pre
-scoped syntax term:max "!" term : sp_pre
-scoped syntax term:max "?" term : sp_pre
-scoped syntax term:max "⊕" term : sp_pre
-scoped syntax "`(SPpre|" sp_pre ")" : term
+declare_syntax_cat spPre
+
+@[inherit_doc Prefix.assign]
+scoped syntax term:max "≔" term : spPre
+
+@[inherit_doc Prefix.sendValue]
+scoped syntax term:max "!" term : spPre
+
+@[inherit_doc Prefix.recvValue]
+scoped syntax term:max "?" term : spPre
+
+@[inherit_doc Prefix.sendLabel]
+scoped syntax term:max "⊕" term : spPre
+
+@[inherit_doc Prefix]
+scoped syntax "`(SPpre|" spPre ")" : term
 
 scoped macro_rules
   | `(`(SPpre| $x:term ≔ $e:term )) => `(Prefix.assign $x $e)
@@ -103,20 +113,32 @@ scoped macro_rules
   | `(`(SPpre| $p:term ? $x:term )) => `(Prefix.recvValue $p $x)
   | `(`(SPpre| $p:term ⊕ $l:term )) => `(Prefix.sendLabel $p $l)
 
-declare_syntax_cat sp_proc
-scoped syntax num : sp_proc
-scoped syntax sp_pre "; " sp_proc : sp_proc
-scoped syntax term:max "&" term : sp_proc
-scoped syntax "if" term "then" sp_proc "else" sp_proc : sp_proc
+declare_syntax_cat spProc
+
+@[inherit_doc Process.nil]
+scoped syntax num : spProc
+
+@[inherit_doc Process.pre]
+scoped syntax spPre "; " spProc : spProc
+
+@[inherit_doc Process.recvLabel]
+scoped syntax term:max "&" term : spProc
+
+@[inherit_doc Process.cond]
+scoped syntax "if" term "then" spProc "else" spProc : spProc
+
 -- The next syntax would be nice to have to avoid having trailing 0s in examples.
--- scoped syntax:min "`(SP| " sp_pre ")" : term
-scoped syntax "`(SP| " sp_proc ")" : term
+-- scoped syntax:min "`(SP| " spPre ")" : term
+
+@[inherit_doc Process]
+scoped syntax "`(SP| " spProc ")" : term
+
 scoped macro_rules
   | `(`(SP| 0)) => `(0)
-  | `(`(SP| $prf:sp_pre; $pr:sp_proc)) => `(Process.pre `(SPpre| $prf) `(SP| $pr))
-  -- | `(`(SP| $prf:sp_pre)) => `(Process.pre `(SPpre| $prf) 0)
+  | `(`(SP| $prf:spPre; $pr:spProc)) => `(Process.pre `(SPpre| $prf) `(SP| $pr))
+  -- | `(`(SP| $prf:spPre)) => `(Process.pre `(SPpre| $prf) 0)
   | `(`(SP| $p:term & $l:term)) => `(Process.recvLabel $p $l)
-  | `(`(SP| if $e:term then $p₁:sp_proc else $p₂:sp_proc)) =>
+  | `(`(SP| if $e:term then $p₁:spProc else $p₂:spProc)) =>
     `(Process.cond $e `(SP| $p₁) `(SP| $p₂))
 
 end Syntax
diff --git a/Cslib/Languages/StatefulProcesses/Network.lean b/Cslib/Languages/StatefulProcesses/Network.lean
index 4ed9d0ef2..61217e93a 100644
--- a/Cslib/Languages/StatefulProcesses/Network.lean
+++ b/Cslib/Languages/StatefulProcesses/Network.lean
@@ -97,7 +97,9 @@ abbrev GlobalStore Pid Var Val := (p : Pid) → LocalStore Var Val
 
 /-- Configurations, consisting of a network and a global store. -/
 structure Cfg (Pid Var Val FunId SelLabel ProcName : Type*) where
+  /-- The network of the configuration. -/
   net : Network Pid Var Val FunId SelLabel ProcName
+  /-- The global store of the configuration. -/
   store : GlobalStore Pid Var Val
 
 /-- Transition labels for network configurations.

From 44bf6f9584207bda96c5a4f05a123ebec4fccd64 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 29 Jul 2026 14:26:08 +0200
Subject: [PATCH 7/7] doc strings

---
 Cslib/Languages/StatefulProcesses/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Cslib/Languages/StatefulProcesses/Basic.lean b/Cslib/Languages/StatefulProcesses/Basic.lean
index 7ed463b9a..5d8a40d83 100644
--- a/Cslib/Languages/StatefulProcesses/Basic.lean
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -90,6 +90,7 @@ inductive Process (Pid Var Val FunId SelLabel ProcName : Type*) where
 
 instance : Zero (Process Pid Var Val FunId SelLabel ProcName) := ⟨.nil⟩
 
+/-- Syntactic category for prefixes. -/
 declare_syntax_cat spPre
 
 @[inherit_doc Prefix.assign]
@@ -113,6 +114,7 @@ scoped macro_rules
   | `(`(SPpre| $p:term ? $x:term )) => `(Prefix.recvValue $p $x)
   | `(`(SPpre| $p:term ⊕ $l:term )) => `(Prefix.sendLabel $p $l)
 
+/-- Syntactic category for processes. -/
 declare_syntax_cat spProc
 
 @[inherit_doc Process.nil]