Dependent session types allow us to describe not only properties of the I/O behavior of processes but also of the exchanged data. In this paper we show how to exploit dependent session types to express proof-carrying communication. We further introduce two modal operators into the type theory to provide detailed control about how much information is communicated: one based on traditional proof irrelevance and one integrating digital signatures.
|Title of host publication||Lecture Notes in Computer Science|
|Publication status||Published - 1 Jan 2011|
|Event||Certified Programs and Proofs - First International Conference, CPP 2011 - |
Duration: 1 Jan 2011 → …
|Conference||Certified Programs and Proofs - First International Conference, CPP 2011|
|Period||1/01/11 → …|
Pfenning, F., Caires, L. M. M. D. C., & Toninho, B. (2011). Proof-Carrying Code in a Session-Typed Process Calculus. In Lecture Notes in Computer Science (pp. 21-36) https://doi.org/10.1007/978-3-642-25379-9_4