Taking Linear Logic Apart

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

60 Downloads (Pure)

Abstrakt

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.

OriginalsprogEngelsk
TitelProceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications
RedaktørerThomas Ehrhard, Maribel Fernández, Valeria de Paiva, Lorenzo Tortora de Falco
Vol/bind292
ForlagOpen Publishing Association
Publikationsdato15. apr. 2019
Sider90-103
DOI
StatusUdgivet - 15. apr. 2019
Begivenhed2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018 - Oxford, Storbritannien
Varighed: 7. jul. 20188. jul. 2018

Konference

Konference2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018
Land/OmrådeStorbritannien
ByOxford
Periode07/07/201808/07/2018
NavnElectronic Proceedings in Theoretical Computer Science, EPTCS
Vol/bind292
ISSN2075-2180

Fingeraftryk

Dyk ned i forskningsemnerne om 'Taking Linear Logic Apart'. Sammen danner de et unikt fingeraftryk.

Citationsformater