Classical Higher-Order Processes - (Short Paper)

Fabrizio Montesi [2017].
In proceedings of FORTE 2017, pp. 171-178.

Classical Processes (CP) is a calculus where the proof theory of classical linear logic types processes `a la π-calculus, building on a Curry-Howard correspondence between session types and linear propositions. We contribute to this research line by extending CP with process mobility, inspired by the Higher-Order π-calculus. The key to our calculus is that sequents are asymmetric: one side types sessions as in CP and the other types process variables, which can be instantiated with process values. The controlled interaction between the two sides ensures that process variables can be used at will, but always respecting the linear usage of sessions expected by the environment.
Additional notes
Cite (BibTeX)
Click to expand
  author       = {Fabrizio Montesi},
  editor       = {Ahmed Bouajjani and
                  Alexandra Silva},
  title        = {Classical Higher-Order Processes - (Short Paper)},
  booktitle    = {Formal Techniques for Distributed Objects, Components, and Systems
                  - 37th {IFIP} {WG} 6.1 International Conference, {FORTE} 2017, Held
                  as Part of the 12th International Federated Conference on Distributed
                  Computing Techniques, DisCoTec 2017, Neuch{\^{a}}tel, Switzerland,
                  June 19-22, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10321},
  pages        = {171--178},
  publisher    = {Springer},
  year         = {2017},
  url          = {\_12},
  doi          = {10.1007/978-3-319-60225-7\_12},
  timestamp    = {Wed, 25 Sep 2019 18:07:00 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

A PDF is available (possibly a preprint):

Download PDF