We define complete type reconstruction algorithms for two type systems ensuring deadlock and lock freedom of linear π-calculus processes. Our work automates the verification of deadlock/lock freedom for a non-trivial class of processes that includes interleaved binary sessions and, to great extent, multiparty sessions as well. A Haskell implementation of the algorithms is available.
Padovani, L., Chen, T.C., Tosatto, A. (2015). Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi. DEU : Springer [10.1007/978-3-319-19282-6_6].
Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi
PADOVANI, Luca;
2015
Abstract
We define complete type reconstruction algorithms for two type systems ensuring deadlock and lock freedom of linear π-calculus processes. Our work automates the verification of deadlock/lock freedom for a non-trivial class of processes that includes interleaved binary sessions and, to great extent, multiparty sessions as well. A Haskell implementation of the algorithms is available.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
