@inbook {IOPORT.05977501,
    author       = {Pfenning, Frank and Caires, Luis and Toninho, Bernardo},
    title        = {Proof-carrying code in a session-typed process calculus.},
    year         = {2011},
    booktitle    = {Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7--9, 2011. Proceedings},
    isbn         = {978-3-642-25378-2},
    pages        = {21-36},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-642-25379-9_4},
    abstract     = {Summary: 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.},
    identifier   = {05977501},
}