Typed ψ-calculi

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

10 Citationer (Scopus)

Resumé

A large variety of process calculi extend the pi-calculus with more general notions of messages. Bengtson et al. have shown that many of these pi-like calculi can be expressed as so-called psi-calculi. In this paper, we describe a simple type system for psi-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed pi-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind6901
Sider (fra-til)265-279
Antal sider15
ISSN0302-9743
DOI
StatusUdgivet - 2011
Begivenhed22nd International Conference on Concurrency Theory - Aachen, Tyskland
Varighed: 6 sep. 20119 sep. 2011
Konferencens nummer: 22

Konference

Konference22nd International Conference on Concurrency Theory
Nummer22
LandTyskland
ByAachen
Periode06/09/201109/09/2011

Bibliografisk note

Proceendings of the 22nd International Conference on Concurrency Theory. Katoen, J.-P. & König, B. (eds.)

Citer dette

@inproceedings{650b7ac7cab34146a7b2d08dd7052dba,
title = "Typed ψ-calculi",
abstract = "A large variety of process calculi extend the pi-calculus with more general notions of messages. Bengtson et al. have shown that many of these pi-like calculi can be expressed as so-called psi-calculi. In this paper, we describe a simple type system for psi-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed pi-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.",
author = "Hans H{\"u}ttel",
note = "Proceendings of the 22nd International Conference on Concurrency Theory. Katoen, J.-P. & K{\"o}nig, B. (eds.)",
year = "2011",
doi = "10.1007/978-3-642-23217-6_18",
language = "English",
volume = "6901",
pages = "265--279",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Physica-Verlag",

}

Typed ψ-calculi. / Hüttel, Hans.

I: Lecture Notes in Computer Science, Bind 6901, 2011, s. 265-279.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

TY - GEN

T1 - Typed ψ-calculi

AU - Hüttel, Hans

N1 - Proceendings of the 22nd International Conference on Concurrency Theory. Katoen, J.-P. & König, B. (eds.)

PY - 2011

Y1 - 2011

N2 - A large variety of process calculi extend the pi-calculus with more general notions of messages. Bengtson et al. have shown that many of these pi-like calculi can be expressed as so-called psi-calculi. In this paper, we describe a simple type system for psi-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed pi-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.

AB - A large variety of process calculi extend the pi-calculus with more general notions of messages. Bengtson et al. have shown that many of these pi-like calculi can be expressed as so-called psi-calculi. In this paper, we describe a simple type system for psi-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed pi-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.

U2 - 10.1007/978-3-642-23217-6_18

DO - 10.1007/978-3-642-23217-6_18

M3 - Conference article in Journal

VL - 6901

SP - 265

EP - 279

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -