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/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
new file mode 100644
index 000000000..5d8a40d83
--- /dev/null
+++ b/Cslib/Languages/StatefulProcesses/Basic.lean
@@ -0,0 +1,198 @@
+/-
+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
+
+set_option linter.style.header false in
+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 (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).
+For recursion, only the syntax is currently implemented. Its semantics will follow a similar
+approach to that for `CCS`.
+
+## Implementation notes
+
+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]
+-/
+
+@[expose] public section
+
+namespace Cslib.StatefulProcesses
+
+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 Prefix (Pid Var Val FunId SelLabel : Type*) where
+  /-- Assign to `x` the result of evaluating `e`. -/
+  | assign (x : Var) (e : Expr Var Val FunId)
+  /-- Send to `p` the result of evaluating `e`. -/
+  | 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)
+
+/-- Processes. -/
+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 : 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 Val FunId SelLabel ProcName))
+  /-- Conditional: evaluate `e` to choose between `pr₁` and `pr₂`. -/
+  | 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 Val FunId SelLabel ProcName) := ⟨.nil⟩
+
+/-- Syntactic category for prefixes. -/
+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)
+  | `(`(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)
+
+/-- Syntactic category for processes. -/
+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| " spPre ")" : term
+
+@[inherit_doc Process]
+scoped syntax "`(SP| " spProc ")" : term
+
+scoped macro_rules
+  | `(`(SP| 0)) => `(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₁:spProc else $p₂:spProc)) =>
+    `(Process.cond $e `(SP| $p₁) `(SP| $p₂))
+
+end Syntax
+
+section Semantics
+
+/-! ## Semantics -/
+
+/-- Actions. -/
+inductive Act (Pid Var Val FunId SelLabel : Type*) where
+  /-- Assign to `x` the result of evaluating `e`. -/
+  | assign (x : Var) (e : Expr Var Val FunId)
+  /-- Send to `p` the result of evaluating `e`. -/
+  | 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`. -/
+  | 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 Var Val FunId)
+  /-- Choose the else-branch of a conditional guarded by `e`. -/
+  | 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
+
+/-- 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
+
+/-- Symbolic transition relation for processes.
+Do not use this directly, use `Process.lts` instead. -/
+inductive Process.Tr :
+    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 Val FunId SelLabel ProcName) (Act Pid Var Val FunId 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..61217e93a
--- /dev/null
+++ b/Cslib/Languages/StatefulProcesses/Network.lean
@@ -0,0 +1,165 @@
+/-
+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.Syntax.HasSubstitution
+
+/-! # 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
+
+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
+
+/-! ## Networks and their symbolic semantics -/
+
+/-- A network maps process names to process terms. -/
+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
+  /-- 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.
+
+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.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
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 7366ab0c2..6af9dafc4 100644
--- a/references.bib
+++ b/references.bib
@@ -1,3 +1,13 @@
+@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,
   author       = {Luca Aceto and
                   Anna Ing{\'{o}}lfsd{\'{o}}ttir},