file.pdf (308.99 kB)
Download file

Proof-Carrying Code in a Session-Typed Process Calculus

Download (308.99 kB)
journal contribution
posted on 01.01.1984, 00:00 authored by Frank Pfenning, Luis Caires, Bernardo Toninho

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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1984