Abstract
This paper investigates the use of symmetric monoidal closed (smc) structure for representing syntax with variable binding, in particular for languages with linear aspects. In this setting, one first specifies an smc theory \({\mathcal{T}}\), which may express binding operations, in a way reminiscent from higher-order abstract syntax (hoas). This theory generates an smc category \(S ({\mathcal{T}}\) whose morphisms are, in a sense, terms in the desired syntax. We apply our approach to Jensen and Milner’s (abstract binding) bigraphs, in which processes behave linearly, but names do not. This leads to an alternative category of bigraphs, which we compare to the original.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barber, A., Gardner, P., Hasegawa, M., Plotkin, G.: From action calculi to linear logic. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414. Springer, Heidelberg (1998)
Bruni, R., Montanari, U.: Cartesian closed double categories, their lambda-notation, and the pi-calculus. In: LICS 1999. IEEE Computer Society, Los Alamitos (1999)
Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)
Coccia, M., Gadducci, F., Montanari, U.: GS·Λ theories: A syntax for higher-order graphs. In: CTCS 2002. ENTCS, vol. 69. Elsevier, Amsterdam (2003)
Damgaard, T., Birkedal, L.: Axiomatizing binding bigraphs. Nordic Journal of Computing 13(1-2) (2006)
Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28 (1989)
Debois, S.: Sortings & bigraphs. PhD thesis, IT University of Copenhagen (2008)
Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 124–138. Springer, Heidelberg (1995)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: LICS 1999. IEEE Computer Society, Los Alamitos (1999)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: LICS 1999. IEEE Computer Society, Los Alamitos (1999)
Garner, R.H.G., Hirschowitz, T., Pardon, A.: Graphical presentations of symmetric monoidal closed theories. CoRR, abs/0810.4420 (2008)
Di Gianantonio, P., Honsell, F., Lenisa, M.: RPO, second-order contexts, and λ-calculus. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 334–349. Springer, Heidelberg (2008)
Girard, J.-Y.: Linear logic. Theoretical Comput. Sci. 50 (1987)
Grohmann, D., Miculan, M.: Directed bigraphs. ENTCS 173 (2007)
Hirschowitz, A., Maggesi, M.: Modules over monads and linearity. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 218–237. Springer, Heidelberg (2007)
Hirschowitz, T., Pardon, A.: Binding bigraphs as symmetric monoidal closed theories. CoRR, abs/0810.4419 (2008)
Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: LICS 1999. IEEE Computer Society, Los Alamitos (1999)
Honsell, F., Miculan, M., Scagnetto, I.: Pi-calculus in (co)inductive-type theory. Theor. Comput. Sci. 253(2) (2001)
Hughes, D.J.D.: Simple free star-autonomous categories and full coherence. ArXiv Mathematics e-prints, math/0506521 (June 2005)
Jensen, O.H., Milner, R.: Bigraphs and mobile processes (revised). Technical Report TR580, University of Cambridge (2004)
Lafont, Y.: Interaction nets. In: POPL. ACM, New York (1990)
Lambek, J., Scott, P.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge (1986)
Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1998)
Melliès, P.-A.: Double categories: a modular model of multiplicative linear logic. Mathematical Structures in Computer Science 12 (2002)
Milner, R.: Bigraphs whose names have multiple locality. Technical Report TR603, University of Cambridge (2004)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100(1) (1992)
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI 1988. ACM, New York (1988)
Rathke, J., Sobocinski, P.: Deconstructing behavioural theories of mobility. In: TCS 2008. Springer, Heidelberg (2008)
Sassone, V., Sobociński, P.: Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing 10(2) (2003)
Sassone, V., Sobociński, P.: Reactive systems over cospans. In: LICS 2005. IEEE Press, Los Alamitos (2005)
Tanaka, M.: Abstract syntax and variable binding for linear binders. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, p. 670. Springer, Heidelberg (2000)
Trimble, T.: Linear logic, bimodules, and full coherence for autonomous categories. PhD thesis, Rutgers University (1994)
Wadsworth, C.: Semantics and pragmatics of the lambda calculus. PhD thesis, University of Oxford (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garner, R., Hirschowitz, T., Pardon, A. (2009). Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs. In: Bravetti, M., Zavattaro, G. (eds) CONCUR 2009 - Concurrency Theory. CONCUR 2009. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04081-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-04081-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04080-1
Online ISBN: 978-3-642-04081-8
eBook Packages: Computer ScienceComputer Science (R0)