@inproceedings{10.1145/3414080.3414109,
    Abstract = {Session types have consolidated as a formalism for the specification and static enforcement of communication protocols. Many different theories of dependent session types have been proposed, some enabling refined specifications on the content of messages, others allowing the structure of the protocols to depend on data exchanged in the protocol itself. In this work we continue a line of research studying the foundations of binary session types. In particular, we propose a variant of the linear {$\pi$}-calculus whose type structure encompasses virtually all dependent session types using just two type constructors: linear channel types and linear dependent pairs. We use Agda not only to formalize the metatheory of the calculus and obtain machine-checked proofs of type soundness, but also as host language in which we implement data-dependent protocols.},
    Address = {New York, NY, USA},
    Author = {Ciccone, Luca and Padovani, Luca},
    BookTitle = {Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming},
    ISBN = {9781450388214},
    Keywords = {Agda, linear {$\pi$}-calculus, dependent session types, binary sessions},
    Location = {Bologna, Italy},
    Publisher = {Association for Computing Machinery},
    Series = {PPDP '20},
    Title = {A Dependently Typed Linear {$\pi$}-Calculus in Agda},
    URL = {https://doi.org/10.1145/3414080.3414109},
    Year = {2020},
    articleno = {8},
    bdsk-url-1 = {https://doi.org/10.1145/3414080.3414109},
    date-added = {2021-01-12 10:25:32 +0100},
    date-modified = {2021-01-12 10:25:32 +0100},
    numpages = {14},
    doi = {10.1145/3414080.3414109}
}

@inproceedings{10.1145/3414080.3414109, Abstract = {Session types have consolidated as a formalism for the specification and static enforcement of communication protocols. Many different theories of dependent session types have been proposed, some enabling refined specifications on the content of messages, others allowing the structure of the protocols to depend on data exchanged in the protocol itself. In this work we continue a line of research studying the foundations of binary session types. In particular, we propose a variant of the linear {$\pi$}-calculus whose type structure encompasses virtually all dependent session types using just two type constructors: linear channel types and linear dependent pairs. We use Agda not only to formalize the metatheory of the calculus and obtain machine-checked proofs of type soundness, but also as host language in which we implement data-dependent protocols.}, Address = {New York, NY, USA}, Author = {Ciccone, Luca and Padovani, Luca}, BookTitle = {Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming}, ISBN = {9781450388214}, Keywords = {Agda, linear {$\pi$}-calculus, dependent session types, binary sessions}, Location = {Bologna, Italy}, Publisher = {Association for Computing Machinery}, Series = {PPDP '20}, Title = {A Dependently Typed Linear {$\pi$}-Calculus in Agda}, URL = {https://doi.org/10.1145/3414080.3414109}, Year = {2020}, articleno = {8}, bdsk-url-1 = {https://doi.org/10.1145/3414080.3414109}, date-added = {2021-01-12 10:25:32 +0100}, date-modified = {2021-01-12 10:25:32 +0100}, numpages = {14}, doi = {10.1145/3414080.3414109} }