TY - GEN
T1 - Depending on session-typed processes
AU - Toninho, Bernardo
AU - Yoshida, Nobuko
N1 - info:eu-repo/grantAgreement/FCT/5876/147239/PT#
The authors would like to thank the anonymous reviews for their comments and suggestions. This work is partially supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1 and NOVA LINCS (UID/CEC/04516/2013).
PY - 2018/1/1
Y1 - 2018/1/1
N2 - This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed λ -calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.
AB - This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed λ -calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.
UR - http://www.scopus.com/inward/record.url?scp=85045681701&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-89366-2_7
DO - 10.1007/978-3-319-89366-2_7
M3 - Conference contribution
AN - SCOPUS:85045681701
SN - 9783319893655
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 128
EP - 145
BT - Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
A2 - Baier, C.
A2 - Dal Lago, U.
PB - Springer Verlag
T2 - 21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Y2 - 14 April 2018 through 20 April 2018
ER -