Abstract
The combination of timed, spatial, and epistemic information is often needed in the specification of modern concurrent systems. We propose the proof system SELL\(^\Cap\), which extends linear logic with subexponentials with quantifiers over subexponentials, therefore allowing for an arbitrary number of modalities. We then show how a proper structure of the subexponential signature in SELL\(^\Cap\) allows for the specification of concurrent systems with timed, spatial, and epistemic modalities. In the context of Concurrent Constraint Programming (CCP), a declarative model of concurrency, we illustrate how the view of subexponentials as specific modalities is general enough to modularly encode into SELL\(^\Cap\) variants of CCP with these three modalities, thus providing a proof-theoretic foundations for those calculi.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation 2(3), 297–347 (1992)
Danos, V., Joinet, J.-B., Schellinx, H.: The structure of exponentials: Uncovering the dynamics of linear logic proofs. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 159–171. Springer, Heidelberg (1993)
Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. JCS 12(2), 247–311 (2004)
Fages, F., Ruet, P., Soliman, S.: Linear concurrent constraint programming: Operational and phase semantics. Information and Computation 165(1), 14–41 (2001)
Gentzen, G.: Investigations into logical deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317–332. Springer, Heidelberg (2012)
Nielsen, M., Palamidessi, C., Valencia, F.D.: Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing 9(1), 145–188 (2002)
Nigam, V.: On the complexity of linear authorization logics. In: LICS, pp. 511–520. IEEE (2012)
Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: PPDP, pp. 129–140. ACM (2009)
Nigam, V., Miller, D.: A framework for proof systems. J. Autom. Reasoning 45(2), 157–188 (2010)
Nigam, V., Pimentel, E., Reis, G.: Specifying proof systems in linear logic with subexponentials. Electr. Notes Theor. Comput. Sci. 269, 109–123 (2011)
Olarte, C., Rueda, C., Valencia, F.D.: Models and emerging trends of concurrent constraint programming. Constraints (2013)
Palamidessi, C., Saraswat, V.A., Valencia, F.D., Victor, B.: On the expressiveness of linearity vs persistence in the asychronous pi-calculus. In: LICS, pp. 59–68. IEEE Computer Society (2006)
Saraswat, V.A., Rinard, M.C., Panangaden, P.: Semantic foundations of concurrent constraint programming. In: POPL, pp. 333–352. ACM (1991)
Saraswat, V.A.: Concurrent Constraint Programming. MIT Press (1993)
Saraswat, V.A., Jagadeesan, R., Gupta, V.: Timed default concurrent constraint programming. J. Symb. Comput. 22(5/6), 475–520 (1996)
Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgments and properties. TR CMU-CS-02-101, CMU (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nigam, V., Olarte, C., Pimentel, E. (2013). A General Proof System for Modalities in Concurrent Constraint Programming. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-40184-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40183-1
Online ISBN: 978-3-642-40184-8
eBook Packages: Computer ScienceComputer Science (R0)