Type inference for correspondence types

Hans Hüttel; Andy Gordon; Rene Rydhof Hansen

doi:doi:10.1016/j.entcs.2009.07.079

Type inference for correspondence types

Hans Hüttel, Andy Gordon, Rene Rydhof Hansen

Department of Computer Science

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

1 Citation (Scopus)

Abstract

We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable.

Original language	English
Title of host publication	Proceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08)
Number of pages	15
Publisher	Elsevier
Publication date	2009
Pages	21-36
DOIs	https://doi.org/doi:10.1016/j.entcs.2009.07.079
Publication status	Published - 2009
Event	International Workshop on Security Issues in Concurrency - Toronto, Canada Duration: 23 Aug 2008 → 23 Aug 2008 Conference number: 6

Conference

Conference	International Workshop on Security Issues in Concurrency
Number	6
Country/Territory	Canada
City	Toronto
Period	23/08/2008 → 23/08/2008

Series	Electronic Notes in Theoretical Computer Science
Number	242
Volume	3
ISSN	1571-0661

Keywords

Types
Process calculi
Type inference
Cryptographic protocols
First order logic

Access to Document

doi:10.1016/j.entcs.2009.07.079

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{b55251906ac711dd92a2000ea68e967b,

title = "Type inference for correspondence types",

abstract = "We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable.",

keywords = "Typer, Proceskalkyler, Typeinferens, Kryptografiske protokoller, F{\o}rste-ordens logik, Types, Process calculi, Type inference, Cryptographic protocols, First order logic",

author = "Hans H{\"u}ttel and Andy Gordon and Hansen, {Rene Rydhof}",

year = "2009",

doi = "doi:10.1016/j.entcs.2009.07.079",

language = "English",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

number = "242",

pages = "21--36",

booktitle = "Proceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08)",

address = "United Kingdom",

note = "International Workshop on Security Issues in Concurrency ; Conference date: 23-08-2008 Through 23-08-2008",

}

Hüttel, H, Gordon, A & Hansen, RR 2009, Type inference for correspondence types. in Proceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08). Elsevier, Electronic Notes in Theoretical Computer Science, no. 242, vol. 3, pp. 21-36, International Workshop on Security Issues in Concurrency, Toronto, Canada, 23/08/2008. https://doi.org/doi:10.1016/j.entcs.2009.07.079

Type inference for correspondence types. / Hüttel, Hans; Gordon, Andy; Hansen, Rene Rydhof.
Proceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08). Elsevier, 2009. p. 21-36 (Electronic Notes in Theoretical Computer Science; No. 242, Vol. 3).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Type inference for correspondence types

AU - Hüttel, Hans

AU - Gordon, Andy

AU - Hansen, Rene Rydhof

N1 - Conference code: 6

PY - 2009

Y1 - 2009

N2 - We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable.

AB - We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable.

KW - Typer

KW - Proceskalkyler

KW - Typeinferens

KW - Kryptografiske protokoller

KW - Første-ordens logik

KW - Types

KW - Process calculi

KW - Type inference

KW - Cryptographic protocols

KW - First order logic

U2 - doi:10.1016/j.entcs.2009.07.079

DO - doi:10.1016/j.entcs.2009.07.079

M3 - Article in proceeding

T3 - Electronic Notes in Theoretical Computer Science

SP - 21

EP - 36

BT - Proceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08)

PB - Elsevier

T2 - International Workshop on Security Issues in Concurrency

Y2 - 23 August 2008 through 23 August 2008

ER -

Type inference for correspondence types

Abstract

Conference

Keywords

Access to Document

AUB Link

Fingerprint

Cite this