Program semantics
with token passing

Koko Muroya(RIMS, Kyoto University)

Linear Logic Winter School (Marseille / hybrid), 28 January 2022

Program semantics with token passing: overview

1.
MELL proof nets
simulating λ-calculus
3.
token-passing
machines4.
token-guided
machines2.
Geometry ofInteraction (GoI)
for proof nets

2

Muroya (RIMS, Kyoto U.)

1. MELL proof nets simulating λ-calculus● “call-by-name” translation● “call-by-value” translation(A ⇒ B) ↦ (!A ⊸ B)

(A ⇒ B) ↦ !(A ⊸ B)

(λx . x) (λy . y)
3Muroya (RIMS, Kyoto U.)

1. MELL proof nets simulating λ-calculus● “call-by-value” translation (A ⇒ B) ↦ !(A ⊸ B)
● cut elimination simulating β-reduction

↝

↝

↝

↝

(λx . x) (λy . y) →β λy . y4

Muroya (RIMS, Kyoto U.)

2. Geometry of Interaction (GoI) for proof nets
● invariant under cut elimination (and β-reduction), as paths

↝

↝

↝

↝

(λx . x) (λy . y) →β λy . y5

Muroya (RIMS, Kyoto U.)

Program semantics with token passing: overview

1.
MELL proof netssimulating λ-calculus
3.
token-passingmachines

4.
token-guidedmachines2.
Geometry ofInteraction (GoI)
for proof nets

6

Muroya (RIMS, Kyoto U.)

2. Token-passing machines● semantics of functional programs● programs represented graphically (typically as proof nets)● evaluation modelled by dynamic computation of the GoI invariant
passing a token around a fixed proof net● pioneering work, with application to compiler construction[Danos & Regnier, TCS 1999] [Mackie, POPL 1995]

7

Muroya (RIMS, Kyoto U.)

2. Token-passing machines● pioneering work
[Danos & Regnier, TCS 1999]

slides from CSL 2017 talkhttps://www.kurims.kyoto-u.ac.jp/~kmuroya/talks/csl17.pdf
8Muroya (RIMS, Kyoto U.)

2. Token-passing machines

passing a token
around a fixedproof net● semantics of functional programs● programs represented graphically (typically as proof nets)● evaluation modelled by dynamic computation of the GoI invariant● pioneering work, with application to compiler construction[Danos & Regnier, TCS 1999] [Mackie, POPL 1995]● variants for effectful programs[Schöpp, APLAS 2011] [Hasuo & Hoshino, LICS 2011] [Hoshino, M. & Hasuo, CSL-LICS 2014, with a follow-up paper in POPL 2016] [DalLago & Hoshino, LICS 2019]● multi-token variants for effectful programs & parallelism [Dal Lago, Faggian, Hasuo & Yoshimizu, CSL-LICS
2014, with follow-up papers in LICS 2015, POPL 2017]● application to high-level synthesis [Ghica, POPL 2007, with follow-up papers in ENTCS 2010, POPL 2011, ICFP 2011]9Muroya (RIMS, Kyoto U.)

Program semantics with token passing: overview

1.
MELL proof nets
simulating λ-calculus
3.
token-passingmachines2.
Geometry ofInteraction (GoI)
for proof nets

4.
token-guidedmachines

passing a token
around a fixed
proof net
10

Muroya (RIMS, Kyoto U.)From without rewriting to with rewriting● token-passing machines● dynamic computation of the GoI invariant

passing a token
around a fixed
proof netwithout rewriting (cut elimination)● Question:
What happens if dynamic rewriting is allowed in token-passing machines?
● Would that speed up token passing, by removing overlapping paths?

↝11

Muroya (RIMS, Kyoto U.)From without rewriting to with rewriting● Question:
What happens if dynamic rewriting is allowed in token-passing machines?
● Answer(s):● It is possible in a principled way, inspired by virtual reduction [Danos & Regnier,
LICS 1993]● The token witnesses & controls possible rewriting!

12

Muroya (RIMS, Kyoto U.)From without rewriting to with rewriting
passing a token around a
fixed proof net● Question:

What happens if dynamic rewriting is allowed in token-passing machines?
● Answer(s):● It is possible in a principled way, inspired by virtual reduction [Danos & Regnier,
LICS 1993]● The token witnesses & controls possible rewriting!

→ token-guided machines

passing a token around a
proof net,with dynamic rewriting
guided by the token
13

Muroya (RIMS, Kyoto U.)

Program semantics with token passing: overview

1.
MELL proof nets
simulating λ-calculus

2.
Geometry ofInteraction (GoI)
for proof nets

3.
token-passingmachines

4.
token-guidedmachines

passing a token
around a fixed
proof net

passing a token around a
proof net,with dynamic rewriting
guided by the token

14

Muroya (RIMS, Kyoto U.)

4. Token-guided machines

passing a token around a
proof net,with dynamic rewriting
guided by the token● semantics of functional programs● programs represented graphically● evaluation modelled by dynamic computation of the GoI invariant,
together with dynamic rewriting of graphs● evaluation strategies represented by the token● variants for λ-calculus with different evaluation strategies[Sinot, TLCS 2005, with a follow-up paper in MSCS 2006] [M. & Ghica, LMCS 2019]● application to proving observational equivalence [M., PhD thesis 2020]15

Muroya (RIMS, Kyoto U.)

4. Token-guided machines● The token
witnesses & controls
possible rewriting!

slides from CSL 2017 talkhttps://www.kurims.kyoto-u.ac.jp/~kmuroya/talks/csl17.pdf

token-passing
machine16

token-guidedmachine
Muroya (RIMS, Kyoto U.)

4. Token-guided machines

passing a token around a
proof net,with dynamic rewriting
guided by the token● semantics of functional programs● programs represented graphically● evaluation modelled by dynamic computation of the GoI invariant,
together with dynamic rewriting of graphs● evaluation strategies represented by the token● variants for λ-calculus with different evaluation strategies[Sinot, TLCS 2005, with a follow-up paper in MSCS 2006] [M. & Ghica, LMCS 2019]● application to proving observational equivalence [M., PhD thesis 2020]17

Muroya (RIMS, Kyoto U.)

4. Token-guided machines● evaluation strategies represented by the token

passing a token around a
proof net,with dynamic rewriting
guided by the token● variants for λ-calculus with different evaluation strategies[Sinot, TLCS 2005, with a follow-up paper in MSCS 2006] [M. & Ghica, LMCS 2019]● DEMO: https://koko-m.github.io/GoI-Visualiser/(λx . x) (λy . y)18

Muroya (RIMS, Kyoto U.)

4. Token-guided machines

passing a token around a
proof net,with dynamic rewriting
guided by the token● application to proving observational equivalence [M., PhD thesis 2020]● local analysis by inspecting the token
Proof of observational equivalence, using locality● what happens to a certain part of a

Proof idea (simplified):
2. prove that the contextual closure R is a simulationprogram during evaluation

Case (3) update of hypernet● how a term interacts with a contextC⋯

G⋯

G?

⋯G↯

RCsound⋯H⋯

H↯P⋯

Hcondition of(G,H)“roidentifb
ustne
relativ
ied:s s”
e to all possible rewrites
Muroya (RIMS, Kyoto U.)

19

Muroya (RIMS, Kyoto U.)

4. Token-guided machines

passing a token around a
proof net,with dynamic rewriting
guided by the token● application to proving observational equivalence [M., PhD thesis 2020]● local analysis by inspecting the token
Proof of observational equivalence, using locality● what happens to a certain part of aprogram
duringevaluation• evaluation
strategies
represented
by the token• “parts”
of aaprogram,
represented● howterm interacts
withasasub-graphs
context

Proof idea (simplified):
2. prove that the contextual closure R is a simulation
Case (3) update of hypernet
C⋯

G

⋯

G?

⋯P

G

↯

(e.g. all parts of a program that refer to the same
Rvariable)

Csound⋯

H⋯

H↯

⋯

H

condition of(G,H)“roidentifbustne
relativ
ied:s s”
e to all possible rewrites
Muroya (RIMS, Kyoto U.)

20

Muroya (RIMS, Kyoto U.)

Program semantics with token passing: overview

1.
MELL proof nets
simulating λ-calculus

2.
Geometry ofInteraction (GoI)
for proof nets

3.
token-passing
machines4.
token-guided
machinespassing a token
around a fixed
proof net

passing a token around a
proof net,with dynamic rewriting
guided by the token

21

Muroya (RIMS, Kyoto U.)

Some research questions● token-guided machines with flexible dynamic rewriting● balancing space/time efficiency?

● proving observational equivalence between effectful programswith token-guided machines (ongoing)● transferring insights to conventional syntactical semantics● cf. syntactical token-passing machines [Accattoli, Dal Lago & Vanoni, PPDP 2020, withfollow-up papers in POPL 2021, LICS 2021]

22

Muroya (RIMS, Kyoto U.)