Classical Processes

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 \pi-calculus.

Typing rules

The rule for multiplicative disjunction ⅋ is

\frac{
	P \vdash \Gamma, x : A, y : B
}{
	y(x).\ P \vdash \Gamma, y : A ⅋ B
}

The rule for multiplicative conjunction \otimes is

\frac{
	P \vdash \Gamma, x : A
  \quad
  Q \vdash \Delta, y : B
}{
	y[x].(P \mid Q) \vdash \Gamma, \Delta
}

The rules for additive disjunction \otimes are

\frac{
	P \vdash \Gamma, x : A
}{
	x[\textsf{inl}].\ P \vdash \Gamma, x : A \oplus B
}
\quad
\frac{
	Q \vdash \Gamma, x : B
}{
	x[\textsf{inr}].\ Q \vdash \Gamma, x : A \oplus B
}

The rule for additive conjunction & are

\frac{
	P \vdash \Gamma, y : A
  \quad
  Q \vdash \Gamma, z : B
}{
	x.\textsf{case}\{y.\, P; z.\, Q\} \vdash \Gamma
}

The rule for the \otimes unit \mathbf{1} is

\frac{
}{
	x[].\ \textsf{stop} \vdash x : \mathbf{1}
}

The rule for the ⅋ unit \bot is

\frac{
	P \vdash \Gamma
}{
	x(). P \vdash \Gamma, x : \bot
}

Adding concurrency

Oddly, the cut elimination procedure for CP is completely deterministic. Thus, even though its terms look like \pi-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.

References

The system of classical processes was first presented by Philip Wadler at ICFP 2012. The following is the journal version of that paper:

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}
}

Adding recursive types to CP is the subject of

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}
}

A notion of observational equivalence for CP is developed and proved fully abstract for the Relational model of Linear Logic is developed by

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}
}

The following paper argues that the conflation of dual connectives of linear logic (e.g. \bot and \mathbf{1}) allows one to regain some concurrent behaviour.

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}

Classical Processes

Typing rules

Adding concurrency

See also

References