In this paper we compare Wadler’s CP calculus for classical linear processes to a linear version of Parigot’s λμ calculus for classical logic. We conclude that linear λμ is “more or less” CP, in that it equationally corresponds to a polarized version of CP. The comparison is made by extending a technique from Melliès and Tabareau’s tensor logic that correlates negation with polarization. The polarized CP, which is written CP± and pronounced “CP more or less,” is an interesting bridge in the landscape of Curry-Howard interpretations of logic.
CITATION STYLE
Paykin, J., & Zdancewic, S. (2016). Linear λμ is CP (more or less). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9600, pp. 273–291). Springer Verlag. https://doi.org/10.1007/978-3-319-30936-1_15
Mendeley helps you to discover research relevant for your work.