Type inference for correspondence types

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-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 languageEnglish
Title of host publicationProceedings of the 6th Workshop on Security Issues in Concurrency (SecCo'08)
Number of pages15
PublisherElsevier
Publication date2009
Pages21-36
DOIs
Publication statusPublished - 2009
EventInternational Workshop on Security Issues in Concurrency - Toronto, Canada
Duration: 23 Aug 200823 Aug 2008
Conference number: 6

Conference

ConferenceInternational Workshop on Security Issues in Concurrency
Number6
CountryCanada
CityToronto
Period23/08/200823/08/2008
SeriesElectronic Notes in Theoretical Computer Science
Number242
Volume3
ISSN1571-0661

    Fingerprint

Keywords

  • Types
  • Process calculi
  • Type inference
  • Cryptographic protocols
  • First order logic

Cite this

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