Adjunct elimination in context logic for trees. (English) Zbl 1200.68224
Summary: We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic.
References:
| [1] | Ishtiaq, S. S.; O’Hearn, P. W., BI as an assertion language for mutable data structures, (POPL 2001 (2001), ACM Press: ACM Press New York), 14-26 · Zbl 1323.68077 |
| [2] | Reynolds, J. C., Separation Logic: a logic for shared mutable data structures, (LICS 2002 (2002), IEEE Computer Society: IEEE Computer Society Los Alamitos), 55-74 |
| [3] | Yang, H.; O’Hearn, P. W., A semantic basis for local reasoning, (Nielsen, M.; Engberg, U., ETAPS 2002 and FOSSACS 2002. ETAPS 2002 and FOSSACS 2002, LNCS, vol. 2303 (2002), Springer: Springer Heidelberg), 402-416 · Zbl 1077.68705 |
| [4] | Cardelli, L.; Gordon, A. D., Anytime anywhere: modal logics for mobile ambients, (POPL 2000 (2000), ACM Press: ACM Press New York), 365-377 · Zbl 1323.68405 |
| [5] | Calcagno, C.; Gardner, P.; Zarfaty, U., Context Logic and tree update, (POPL 2005 (2005), ACM Press: ACM Press New York), 271-282 · Zbl 1369.68132 |
| [6] | Calcagno, C.; Gardner, P.; Zarfaty, U., Context logic as modal logic: completeness and parametric inexpressivity, (POPL 2007 (2007), ACM Press: ACM Press New York), 123-134 · Zbl 1295.68079 |
| [7] | Lozes, E., Adjuncts elimination in the static Ambient Logic, (Corradini, F.; Nestmann, U., EXPRESS 2003. EXPRESS 2003, ENTCS, vol. 96 (2003), Elsevier: Elsevier Amsterdam), 51-72 · Zbl 1271.03050 |
| [8] | Dawar, A.; Gardner, P.; Ghelli, G., Adjunct elimination through games in static Ambient Logic, (Lodaya, K.; Mahajan, M., FSTTCS 2004. FSTTCS 2004, LNCS, vol. 3328 (2004), Springer: Springer Heidelberg), 211-223 · Zbl 1117.03338 |
| [11] | Calcagno, C.; Dinsdale-Young, T.; Gardner, P., Adjunct elimination in Context Logic for trees, (APLAS 2007. APLAS 2007, LNCS (2007), Springer: Springer Heidelberg), 255-270 · Zbl 1137.03312 |
| [12] | O’Hearn, P.; Pym, D., Logic of bunched implications, Bulletin of Symbolic Logic, 5, 2, 215-244 (1999) · Zbl 0930.03095 |
| [13] | Heuter, U., First-order properties of trees, star-free expressions, and aperiodicity, Informatique Théorique et Applications, 25, 2, 125-145 (1991) · Zbl 0741.68065 |
| [14] | Bojańczyk, M., Forest expressions, (Duparc, J.; Henzinger, T. A., CSL 2007. CSL 2007, LNCS, vol. 4646 (2007), Springer: Springer Heidelberg), 146-160 · Zbl 1179.68068 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
