Sessions as Propositions
Programming Languages
2014-06-16 v1 Distributed, Parallel, and Cluster Computing
Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1406.3479,
title = {Sessions as Propositions},
author = {Sam Lindley and J. Garrett Morris},
journal= {arXiv preprint arXiv:1406.3479},
year = {2014}
}
Comments
In Proceedings PLACES 2014, arXiv:1406.3313