Proof-Carrying Code in a Session-Typed Process Calculus

Frank Pfenning; Luís Manuel Marques da Costa Caires; Bernardo Toninho

doi:10.1007/978-3-642-25379-9_4

Proof-Carrying Code in a Session-Typed Process Calculus

Frank Pfenning, Luís Manuel Marques da Costa Caires, Bernardo Toninho

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

22 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 language	Unknown
Title of host publication	Lecture Notes in Computer Science
Pages	21-36
DOIs	https://doi.org/10.1007/978-3-642-25379-9_4
Publication status	Published - 1 Jan 2011
Event	Certified Programs and Proofs - First International Conference, CPP 2011 - Duration: 1 Jan 2011 → …

Conference

Conference	Certified Programs and Proofs - First International Conference, CPP 2011
Period	1/01/11 → …

Access to Document

10.1007/978-3-642-25379-9_4

Cite this

@inproceedings{c9622c2428c347299a763cd4b2399796,

title = "Proof-Carrying Code in a Session-Typed Process Calculus",

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.",

author = "Frank Pfenning and Caires, \{Lu{\'i}s Manuel Marques da Costa\} and Bernardo Toninho",

year = "2011",

month = jan,

day = "1",

doi = "10.1007/978-3-642-25379-9\_4",

language = "Unknown",

isbn = "978-3-642-25378-2",

pages = "21--36",

booktitle = "Lecture Notes in Computer Science",

note = "Certified Programs and Proofs - First International Conference, CPP 2011 ; Conference date: 01-01-2011",

}

TY - GEN

T1 - Proof-Carrying Code in a Session-Typed Process Calculus

AU - Pfenning, Frank

AU - Caires, Luís Manuel Marques da Costa

AU - Toninho, Bernardo

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-25379-9_4

DO - 10.1007/978-3-642-25379-9_4

M3 - Conference contribution

SN - 978-3-642-25378-2

SP - 21

EP - 36

BT - Lecture Notes in Computer Science

T2 - Certified Programs and Proofs - First International Conference, CPP 2011

Y2 - 1 January 2011

ER -