On session types and polynomial time

被引：6

作者：

Dal Lago, Ugo ^{[1
,2
]}

Di Giamberardino, Paolo ^{[3
]}

机构：

[1] Univ Bologna, Mura Anteo Zamboni 7, I-40127 Bologna, Italy

[2] INRIA Sophia Antipolis, Mura Anteo Zamboni 7, I-40127 Bologna, Italy

[3] Univ Cagliari, Dipartimento Matemat & Informat, Via Osped 72, I-09124 Cagliari, Italy

来源：

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2016年 / 26卷 / 08期

关键词：

D O I：

10.1017/S0960129514000632

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We show how systems of session types can enforce interactions to take bounded time 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 reduction sequences starting from it and on the size of its reducts.

引用

页码：1433 / 1458

页数：26

共 16 条

[1]

Baillot P, 2004, LECT NOTES COMPUT SC, V2987, P27

[2]

Caires L, 2013, LECT NOTES COMPUT SC, V7792, P330, DOI 10.1007/978-3-642-37036-6_19

[3]

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

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

Dal Lago, Ugo ;

Baillot, Patrick .

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

[5] Soft Session Types [J].

Dal Lago, Ugo ;

Di Giamberardino, Paolo .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (64) :59-73

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

Dal Lago, Ugo ;

Martini, Simone ;

Sangiorgi, Davide .

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

[7] Quantum implicit computational complexity [J].

Dal Lago, Ugo ;

Masini, Andrea ;

Zorzi, Margherita .

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

[8] LINEAR LOGIC [J].

GIRARD, JY .

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

[9]

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

[10] Multiparty Asynchronous Session Types [J].

Honda, Kohei ;

Yoshida, Nobuko ;

Carbone, Marco .

JOURNAL OF THE ACM, 2016, 63 (01)

← 1 2 →