Depending on session-typed processes

Bernardo Toninho, Nobuko Yoshida

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFoundations 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
EditorsC. Baier, U. Dal Lago
PublisherSpringer Verlag
Pages128-145
Number of pages18
ISBN (Print)9783319893655
DOIs
Publication statusPublished - 1 Jan 2018
Event21st 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 - Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Volume10803 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st 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
CountryGreece
CityThessaloniki
Period14/04/1820/04/18

Fingerprint

Calculus
Monads
Dependent
Type Theory
Communication
Expressiveness
Soundness
Faithful
Predicate
Verify
Framework

Cite this

Toninho, B., & Yoshida, N. (2018). Depending on session-typed processes. In C. Baier, & U. Dal Lago (Eds.), 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 (pp. 128-145). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10803 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-89366-2_7
Toninho, Bernardo ; Yoshida, Nobuko. / Depending on session-typed processes. 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. editor / C. Baier ; U. Dal Lago. Springer Verlag, 2018. pp. 128-145 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c1a527ce623a4a63baeb4f69b8e31b5f,
title = "Depending on session-typed processes",
abstract = "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.",
author = "Bernardo Toninho and Nobuko Yoshida",
note = "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).",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-319-89366-2_7",
language = "English",
isbn = "9783319893655",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "128--145",
editor = "C. Baier and {Dal Lago}, U.",
booktitle = "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",
address = "Germany",

}

Toninho, B & Yoshida, N 2018, Depending on session-typed processes. in C Baier & U Dal Lago (eds), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10803 LNCS, Springer Verlag, pp. 128-145, 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, Thessaloniki, Greece, 14/04/18. https://doi.org/10.1007/978-3-319-89366-2_7

Depending on session-typed processes. / Toninho, Bernardo; Yoshida, Nobuko.

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. ed. / C. Baier; U. Dal Lago. Springer Verlag, 2018. p. 128-145 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10803 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

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

ER -

Toninho B, Yoshida N. Depending on session-typed processes. In Baier C, Dal Lago U, editors, 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. Springer Verlag. 2018. p. 128-145. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-89366-2_7