Classical higher-order processes

Fabrizio Montesi*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

175 Downloads (Pure)

Abstract

Classical Processes (CP) is a calculus where the proof theory of classical linear logic types processes à 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.

Original languageEnglish
Title of host publicationFormal 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, Proceedings
EditorsAhmed Bouajjani, Alexandra Silva
PublisherSpringer
Publication date2017
Pages171-178
ISBN (Print)9783319602240
ISBN (Electronic)978-3-319-60225-7
DOIs
Publication statusPublished - 2017
Event37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017 - Neuchatel, Switzerland
Duration: 19. Jun 201722. Jun 2017

Conference

Conference37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017
Country/TerritorySwitzerland
CityNeuchatel
Period19/06/201722/06/2017
SeriesLecture Notes in Computer Science
Volume10321
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Classical higher-order processes'. Together they form a unique fingerprint.

Cite this