Type inference for correspondence types

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

1 Citationer (Scopus)

Abstrakt

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.
OriginalsprogEngelsk
TitelProceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08)
Antal sider15
ForlagElsevier
Publikationsdato2009
Sider21-36
DOI
StatusUdgivet - 2009
BegivenhedInternational Workshop on Security Issues in Concurrency - Toronto, Canada
Varighed: 23 aug. 200823 aug. 2008
Konferencens nummer: 6

Konference

KonferenceInternational Workshop on Security Issues in Concurrency
Nummer6
LandCanada
ByToronto
Periode23/08/200823/08/2008
NavnElectronic Notes in Theoretical Computer Science
Nummer242
Vol/bind3
ISSN1571-0661

Emneord

  • Typer
  • Proceskalkyler
  • Typeinferens
  • Kryptografiske protokoller
  • Første-ordens logik

Fingeraftryk Dyk ned i forskningsemnerne om 'Type inference for correspondence types'. Sammen danner de et unikt fingeraftryk.

Citationsformater