Soft Session Types

被引：5

作者：

Dal Lago, Ugo ^{[1
]}

Di Giamberardino, Paolo ^{[2
]}

机构：

[1] Univ Bologna, INRIA Sophia Antipolis, Bologna, Italy

[2] Lab Informat Paris Nord, Paris, France

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2011年 / 64期

关键词：

D O I：

10.4204/EPTCS.64.5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We show how systems of session types can enforce interactions to be bounded for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of any reduction sequence starting from it and on the size of any of its reducts.

引用

页码：59 / 73

页数：15

共 13 条

[1]

Caires L, 2010, LECT NOTES COMPUT SC, V6269, P222, DOI 10.1007/978-3-642-15375-4_16

[2]

Caires Luis, 2011, PPDP 2011 IN PRESS

[3] On light logics, uniform encodings and polynomial time [J].

Dal Lago, Ugo ;

Baillot, Patrick .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (04) :713-733

[4] Light Logics and Higher-Order Processes [J].

Dal Lago, Ugo ;

Martini, Simone ;

Sangiorgi, Davide .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (41) :46-60

[5] Quantum implicit computational complexity [J].

Dal Lago, Ugo ;

Masini, Andrea ;

Zorzi, Margherita .

THEORETICAL COMPUTER SCIENCE, 2010, 411 (02) :377-409

[6] LINEAR LOGIC [J].

GIRARD, JY .

THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102

[7]

Honda K, 1998, LECT NOTES COMPUT SC, V1381, P122, DOI 10.1007/BFb0053567

[8] Multiparty Asynchronous Session Types [J].

Honda, Kohei ;

Yoshida, Nobuko ;

Carbone, Marco .

POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, :273-284

[9] Soft linear logic and polynomial time [J].

Lafont, Y .

THEORETICAL COMPUTER SCIENCE, 2004, 318 (1-2) :163-180

[10]

Lago Ugo Dal, SOFT SESSION TYPES

← 1 2 →