Sessions as Propositions

Sam Lindley; J.Garrett Morris

doi:10.4204/EPTCS.155.2

Sessions as Propositions

Sam Lindley, J.Garrett Morris

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

Original language	English
Title of host publication	Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)
DOIs	https://doi.org/10.4204/EPTCS.155.2
Publication status	Published - 13 Jun 2014
Event	6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software - Grenoble, France Duration: 12 Apr 2013 → 12 Apr 2013

Workshop

Workshop	6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
Country/Territory	France
City	Grenoble
Period	12/04/13 → 12/04/13

Access to Document

10.4204/EPTCS.155.2

Lindley and Morris 2014 Sessions as PropositionsAccepted author manuscript, 69 KB

http://eptcs.web.cse.unsw.edu.au/paper.cgi?PLACES2014.2

From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P.
EPSRC
20/05/13 → 19/11/20
Project: Research

Cite this

@inproceedings{9d837c31ef1642b29f5de516bba47e1d,

title = "Sessions as Propositions",

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",

author = "Sam Lindley and J.Garrett Morris",

year = "2014",

month = jun,

day = "13",

doi = "10.4204/EPTCS.155.2",

language = "English",

booktitle = "Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)",

note = "6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software ; Conference date: 12-04-2013 Through 12-04-2013",

}

TY - GEN

T1 - Sessions as Propositions

AU - Lindley, Sam

AU - Morris, J.Garrett

PY - 2014/6/13

Y1 - 2014/6/13

N2 - 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

AB - 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

U2 - 10.4204/EPTCS.155.2

DO - 10.4204/EPTCS.155.2

M3 - Conference contribution

BT - Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)

T2 - 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software

Y2 - 12 April 2013 through 12 April 2013

ER -

Sessions as Propositions

Abstract

Workshop

Access to Document

Projects

From Data Types to Session Types - A Basis for Concurrency and Distribution

Cite this