2014/06/13 by Sam Lindley, J. Garrett Morris
Computer Science · #cs.PL #cs.DC #cs.LO
paper · pdf · doi:10.4204/eptcs.155.2
published as EPTCS 155, 2014, pp. 9-16 · In Proceedings PLACES 2014, arXiv:1406.3313
arxiv created 2014/06/13 · arxiv updated 2014/06/16
Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.