Field note
Session Types: One Settlement Story, Three Local Views
Petri nets describe resources and legal transitions well, but a settlement also has distinct participants with different knowledge. The maker publishes terms. The taker claims, pays, and proves. The notary joins a cryptographic session and signs a commitment. No participant sees the entire private execution.
Multiparty session types model this as one global type: a choreography stating the legal message order and branch ownership. A projection derives a local type for each role. If every participant implements its projection, the protocol can guarantee communication fidelity and rule out broad classes of mismatched sends, receives, and deadlocks.
A small choreography
A simplified operational flow is:
Maker -> Network: Post
Taker -> Vault: Claim
Taker <-> Notary <-> Bank: direct MPC-TLS session
Notary -> Taker: attestation over blinded commitment
Taker -> Aggregator: Solve proof
The maker's local program should not wait for a plaintext bank record it will never receive. The notary's local program should not learn the fields it only helps commit. The taker's local program must not display irreversible payment instructions before preflight establishes the currently available evidence path.
Protocol state and operational state differ
The on-vault offer has only Open and Claimed. Network connection, bank login, proof generation, and submission can have loading, retryable failure, and recovery states because those are operational machines with I/O.
Session types help keep those layers from collapsing. A retry in the notary session is not a new offer transition. A bank timeout is not a Failed offer constructor. Only a valid Action changes the resource marking.
The logical connection
Session types have a deep correspondence with linear logic. Sending transfers a capability; receiving acquires it; a channel endpoint must be used according to its protocol rather than copied freely. That same no-copy/no-drop discipline underlies resource conservation.
The result is complementary coverage. The Petri/resource model accounts for every value object and legal state transition. The session type accounts for communication between principals. Treating them as separate views of one protocol makes it harder for a correct circuit and an incorrect wallet choreography to drift apart unnoticed.