Article contents
On session types and polynomial time
Published online by Cambridge University Press: 14 January 2015
Abstract
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.
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 26 , Special Issue 8: Special Issue: Express'11 , December 2016 , pp. 1433 - 1458
- Copyright
- Copyright © Cambridge University Press 2015
References
- 2
- Cited by