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 π-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.

A Dependently-Typed Linear π -Calculus in Agda

Luca Ciccone;Luca Padovani
2020

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 π-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.
International Symposium on Principles and Practice of Declarative Programming
Bologna, Italy
8-10 September 2020
Proceedings of the 22st International Symposium on Principles and Practice of Programming Languages 2020
ACM
1
14
linear π -calculus, dependent session types, binary sessions, Agda
Luca Ciccone; Luca Padovani
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 666.71 kB
Formato Adobe PDF
666.71 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/1739403
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact