Proof-Carrying Code in a Session-Typed Process Calculus
Frank Pfenning
Luis Caires
Bernardo Toninho
10.1184/R1/6608693.v1
https://kilthub.cmu.edu/articles/journal_contribution/Proof-Carrying_Code_in_a_Session-Typed_Process_Calculus/6608693
<p>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.</p>
1984-01-01 00:00:00
Process calculus
session types
proof irrelevance
proofcarrying code