Classical processes (CP) is the name used to refer to a term assignment system for Classical Linear Logic (CLL) presented by Philip Wadler.
The terms of CP are a linearization of CLL proofs. They are called processes because of their similarity with the -calculus.
The rule for multiplicative disjunction is
The rule for multiplicative conjunction is
The rules for additive disjunction are
The rule for additive conjunction & are
The rule for the unit is
The rule for the unit is
Oddly, the cut elimination procedure for CP is completely deterministic. Thus, even though its terms look like -calculus processes, no concurrency is possible.
One of the major 'open problems' is that of re-introducing concurrent behaviour to CP. See for example [Atkey et al. 2016].
Wadler, Philip. 2014. ‘Propositions as Sessions’. Journal of Functional Programming 24 (2–3): 384–418. https://doi.org/10.1017/S095679681400001X.
@article{wadler_propositions_2014,
title = {Propositions as sessions},
volume = {24},
issn = {0956-7968},
doi = {10.1017/S095679681400001X},
number = {2-3},
journal = {Journal of Functional Programming},
author = {Wadler, Philip},
year = {2014},
pages = {384--418}
}
Lindley, Sam, and J. Garrett Morris. 2016. ‘Talking Bananas: Structural Recursion for Session Types’. ACM SIGPLAN Notices 51 (9): 434–47. https://doi.org/10.1145/3022670.2951921.
@article{lindley_talking_2016,
title = {Talking bananas: structural recursion for session types},
volume = {51},
issn = {0362-1340, 1558-1160},
shorttitle = {Talking bananas},
url = {https://dl.acm.org/doi/10.1145/3022670.2951921},
doi = {10.1145/3022670.2951921},
language = {en},
number = {9},
urldate = {2020-05-07},
journal = {ACM SIGPLAN Notices},
author = {Lindley, Sam and Morris, J. Garrett},
month = dec,
year = {2016},
pages = {434--447}
}
Atkey, Robert. 2017. ‘Observed Communication Semantics for Classical Processes’. In Programming Languages and Systems. ESOP 2017, edited by Hongseok Yang, 56–82. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-54434-1_3.
@inproceedings{atkey_observed_2017,
title = {Observed {Communication} {Semantics} for {Classical} {Processes}},
doi = {10.1007/978-3-662-54434-1_3},
booktitle = {Programming {Languages} and {Systems}. {ESOP} 2017},
publisher = {Springer, Berlin, Heidelberg},
author = {Atkey, Robert},
editor = {Yang, Hongseok},
year = {2017},
pages = {56--82}
}
Atkey, Robert, Sam Lindley, and J. Garrett Morris. 2016. ‘Conflation Confers Concurrency’. In A List of Successes That Can Change the World, edited by Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, 9600:32–55. Lecture Notes in Computer Science. Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-30936-1_2.
@incollection{lindley_conflation_2016,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Conflation {Confers} {Concurrency}},
volume = {9600},
isbn = {978-3-319-30935-4},
language = {en},
booktitle = {A {List} of {Successes} {That} {Can} {Change} the {World}},
publisher = {Springer International Publishing},
author = {Atkey, Robert and Lindley, Sam and Morris, J. Garrett},
editor = {Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don},
year = {2016},
note = {doi: 10.1007/978-3-319-30936-1\_2},
pages = {32--55}