Proof-Carrying Code in a Session-Typed Process Calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Citations (Scopus)

Abstract

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.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
Pages21-36
DOIs
Publication statusPublished - 1 Jan 2011
EventCertified Programs and Proofs - First International Conference, CPP 2011 -
Duration: 1 Jan 2011 → …

Conference

ConferenceCertified Programs and Proofs - First International Conference, CPP 2011
Period1/01/11 → …

Cite this