Sessions as Propositions

Sam Lindley; J. Garrett Morris

doi:10.4204/EPTCS.155.2

Sessions as Propositions

Sam Lindley, J. Garrett Morris

Research output: Contribution to conference › Paper › peer-review

2 Citations (Scopus)

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
Pages	9-16
Number of pages	8
DOIs	https://doi.org/10.4204/EPTCS.155.2
Publication status	Published - 2014
Event	7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software 2014 - Grenoble, France Duration: 12 Apr 2014 → 12 Apr 2014

Conference

Conference	7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software 2014
Abbreviated title	PLACES 2014
Country/Territory	France
City	Grenoble
Period	12/04/14 → 12/04/14

Access to Document

10.4204/EPTCS.155.2

Cite this

@conference{224c81a2cb0449d3af0f45ae2eb7781f,

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 Morris, {J. Garrett}",

year = "2014",

doi = "10.4204/EPTCS.155.2",

language = "English",

pages = "9--16",

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

}

TY - CONF

T1 - Sessions as Propositions

AU - Lindley, Sam

AU - Morris, J. Garrett

PY - 2014

Y1 - 2014

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

SP - 9

EP - 16

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

Y2 - 12 April 2014 through 12 April 2014

ER -

Sessions as Propositions

Abstract

Conference

Access to Document

Fingerprint

Cite this