Abstract
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.
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
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001, ACM Press, New York (2001)
Reynolds, J.C.: Separation Logic: a logic for shared mutable data structures. In: LICS 2002, IEEE Computer Society, Los Alamitos (2002)
Yang, H., O’Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, Springer, Heidelberg (2002)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: POPL 2000, ACM Press, New York (2000)
Calcagno, C., Gardner, P., Zarfaty, U.: Context Logic and tree update. In: POPL 2005, ACM Press, New York (2005)
O’Hearn, P., Pym, D.: Logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: POPL 2007, ACM Press, New York (2007)
Lozes, E.: Adjuncts elimination in the static Ambient Logic. In: Corradini, F., Nestmann, U. (eds.) EXPRESS 2003. ENTCS, vol. 96, Elsevier, Amsterdam (2003)
Dawar, A., Gardner, P., Ghelli, G.: Adjunct elimination through games in static Ambient Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, Springer, Heidelberg (2004)
Calcagno, C., Gardner, P., Zarfaty, U.: Separation Logic, Ambient Logic and Context Logic: parametric inexpressivity results (Unpublished, 2006)
Dinsdale-Young, T.: Adjunct elimination in Context Logic. Master’s thesis, Imperial College London (2006)
Heuter, U.: First-order properties of trees, star-free expressions, and aperiodicity. Informatique théorique et applications 25(2), 125–145 (1991)
Bojańczyk, M.: Forest expressions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calcagno, C., Dinsdale-Young, T., Gardner, P. (2007). Adjunct Elimination in Context Logic for Trees. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-76637-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76636-0
Online ISBN: 978-3-540-76637-7
eBook Packages: Computer ScienceComputer Science (R0)