Higher category models of the pi-calculus
Logic in Computer Science
2015-09-23 v4
Abstract
We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an explicit interpretation of the rewrite rules of standard operational presentations as 2-morphisms. One of the key contributions, inspired by catalysis in chemical reactions, is a method of restricting the application of 2-morphisms interpreting rewrites to specific contexts.
Keywords
Cite
@article{arxiv.1504.04311,
title = {Higher category models of the pi-calculus},
author = {Mike Stay and Lucius Gregory Meredith},
journal= {arXiv preprint arXiv:1504.04311},
year = {2015}
}