Translating λ-terms to processes...

[np]

This is an attempt at translating λ-terms to processes it does not work yet.
I'm welcoming your insights.

_° : Typ → Session
(A → B)° = A° -o B°
(A × B)° = [A°, B°]
Int°     = !Int

(_:_)° : (A : Typ) → (t : A) → < A° >
(t : A)° = proc (c : A°) (A, t, c)°

(_,_,_)° : (A : Typ) → (t : A) → c : A°
(A × B,t,c)° = c[c0,c1] ((A,fst t,c0)° | (B,snd t,c1)°)
(A → B,t,c)° = c{i,o} π(A,x,i). (B,t x,o)°
(Int  ,t,c)° = send c t

π(_,_,_) : (A : Typ) → (x : A)× i : ~A°
π(Int,  x,i) = recv i (x : Int)
π(B × C,x,i) = i{i0,i1} (π(B,x0,i0) | π(C,x1,i1)). let x = (x0,x1)
  -- Ok, we don't have `let` as a prefix yet...
π(B → C,x,i) = i[i0,o0] ... no clue ...
  -- A = B → C
  -- A° = {~B°, C°}
  -- ~A° = [B°, ~C°]
  -- i : ~A°
  -- i0 : B°
  -- o0 : ~C°

If terms are kept in normal form, constructs such as fst t,
snd t, and t x above can be reduced on the fly.

(Int → Int → Int, λx→ λy→ x+y, c)° =
  c{i0,io}
  recv i0 (x : Int).
  io{i1,o}
  recv i1 (y : Int).
  send o (x + y)

((Int × Int) → Int, λx→ fst x + snd x, c)° =
  c{i,o}
  i{i0,i1}
  ( recv i0 (x0 : Int)
  | recv i1 (x1 : Int) ).
  let x = (x0,x1)
  send o (fst x + snd x).

(Int → (Int × Int), (λx→(x,x)), c)° =
  c{i,o}
  recv i (x : Int).
  o[c0,c1]
  ( send c0 x
  | send c1 x)

(Int, (λx→ x) 1, c)° =
  send c ((λx→ x) 1)

π(Int → Int, x, i) =
  i[c0,c1]
  ( send c0 1
  | c1 <-> o)

((Int → Int) → Int, λf→ f 1, c)° =
  c{i,o}
  i[c0,c1]
  ( send c0 1
  | c1 <-> o)

(Int → (Int → Int) → Int, λx→ λf→ f x, c)° =
  c{i0,io}
  recv i0 (x : Int).
  io{i1,o}
  i1[c0,c1]
  ( send c0 x
  | c1 <-> o)