3 ms·

> generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How wou

> generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reduction to cut-elimination and parallel composition, and what is meant by hiding here? I would be curious to know of relevant work in the area.

GregarianChild 6y ago
The generalisation of Curry-Howard to parallelism was outlined in early interpretations of linear logic, I think Abramsky's [1] was the first, there has been a lot more work in this direction since. A good place to start to understand the relationship between functional and concurrent computation is Milner's Functions as Processes [2], it's incredibly simple, my mind was blown when I understood it (if you understand CPS transforms, you will find it natural, indeed, I'd say the Milner translation is the essence of CPS, see also [4]). A Curry-Howard correspondence of sorts has now been produced for linear logic and session-typable name passing processes [3]. [1] S. Abramsky, Computational Interpretations of Linear Logic. https://www.sciencedirect.com/science/article/pii/030439759390181R https://www.sciencedirect.com/science/article/pii/0304397593... [2] R. Milner, Functions as Processes. https://hal.inria.fr/inria-00075405/document https://hal.inria.fr/inria-00075405/document [3] L. Caires, F. Pfenning, Session Types as Intuitionistic Linear Propositions. https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.220.3453&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22... [4] H. Thielecke, Continuations, functions and jumps. https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf
- siraben 6y ago
  Thanks! What sort of work did you do in the field of applying categorical methods to programming?

GregarianChild 6y ago

The generalisation of Curry-Howard to parallelism was outlined in early interpretations of linear logic, I think Abramsky's [1] was the first, there has been a lot more work in this direction since. A good place to start to understand the relationship between functional and concurrent computation is Milner's Functions as Processes [2], it's incredibly simple, my mind was blown when I understood it (if you understand CPS transforms, you will find it natural, indeed, I'd say the Milner translation is the essence of CPS, see also [4]). A Curry-Howard correspondence of sorts has now been produced for linear logic and session-typable name passing processes [3]. [1] S. Abramsky, Computational Interpretations of Linear Logic. https://www.sciencedirect.com/science/article/pii/030439759390181R https://www.sciencedirect.com/science/article/pii/0304397593... [2] R. Milner, Functions as Processes. https://hal.inria.fr/inria-00075405/document https://hal.inria.fr/inria-00075405/document [3] L. Caires, F. Pfenning, Session Types as Intuitionistic Linear Propositions. https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.220.3453&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22... [4] H. Thielecke, Continuations, functions and jumps. https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf

siraben 6y ago
Thanks! What sort of work did you do in the field of applying categorical methods to programming?