{- type of channel to interact with processes that represent lists of strings -}
type StringList = (rec L = ^[^[] ^[String L]])

{- process representing the empty list located at channel l -}
def Nil l : ^[^[] ^[String StringList]] = l?[n c] = n![]

{- process representing the list with head string hd and with tail the
   list located at channel tl, located at channel l -}
def Cons[hd : String tl : StringList l : ^[^[] ^[String StringList]]] = 
    l?[n c] = c ! [hd tl]

{- prints the elements of the list localed at channel l -}
def Print l : ^[^[] ^[String StringList]] =
  (new n : ^[] 
   new c : ^[String StringList]
   ( l![n c]
   | n?[] = ()
   | c?[hd (rec tl)] = (print!hd | Print!tl)))

new l1 : ^[^[] ^[String StringList]]
new l2 : ^[^[] ^[String StringList]]
new l3 : ^[^[] ^[String StringList]]
run(Nil!l1 | Cons!["World" (rec l1) l2] | Cons!["Hello" (rec l2) l3] | Print!l3)