Taking Linear Logic Apart

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

58 Downloads (Pure)

Abstract

Process calculi based on logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the π-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. [12] introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP , a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP supports the same communication protocols as CP.

Original languageEnglish
Title of host publicationProceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications
EditorsThomas Ehrhard, Maribel Fernández, Valeria de Paiva, Lorenzo Tortora de Falco
Volume292
PublisherOpen Publishing Association
Publication date15. Apr 2019
Pages90-103
DOIs
Publication statusPublished - 15. Apr 2019
Event2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018 - Oxford, United Kingdom
Duration: 7. Jul 20188. Jul 2018

Conference

Conference2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018
CountryUnited Kingdom
CityOxford
Period07/07/201808/07/2018
SeriesElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume292
ISSN2075-2180

Keywords

  • Curry-Howard correspondence
  • Deadlock-freedom
  • Logic
  • Linear logic
  • Process calculi
  • Programming Languages
  • Formal methods

Fingerprint Dive into the research topics of 'Taking Linear Logic Apart'. Together they form a unique fingerprint.

Cite this