Polymorphic Session Processes as Morphisms

Bernardo Toninho, Nobuko Yoshida

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

The study of expressiveness of concurrent processes via session types opens a connection between linear logic and mobile processes, grounded in the rigorous logical background of propositions-as-types. One such study includes a notion of parametric session polymorphism, which connects session typed processes with rich higher-order functional computations. This work proposes a novel and non-trivial application of session parametricity – an encoding of inductive and coinductive session types, justified via the theory of initial algebras and final co-algebras using a processes-as-morphisms viewpoint. The correctness of the encoding (i.e. universality) relies crucially on parametricity and the associated relational lifting of sessions.

Original languageEnglish
Title of host publicationThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
EditorsM. Alvim, K. Chatzikokolakis, C. Olarte, F. Valencia
PublisherSpringer Verlag
Pages101-117
Number of pages17
ISBN (Electronic)978-3-030-31175-9
ISBN (Print)978-3-030-31174-2
DOIs
Publication statusPublished - 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Volume11760 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Expressiveness
  • F-Algebra
  • Linear logic
  • Session types
  • π -calculus

Fingerprint Dive into the research topics of 'Polymorphic Session Processes as Morphisms'. Together they form a unique fingerprint.

Cite this