Generalized bounded linear logic and its categorical semantics. (English) Zbl 07410427
Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12650, 226-246 (2021).
Summary: We introduce a generalization of Girard et al.’s BLL called GBLL (and its affine variant GBAL). It is designed to capture the core mechanism of dependency in BLL, while it is also able to separate complexity aspects of BLL. The main feature of GBLL is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in GBLL, and give a translation from BLL with constraints to GBAL with positivity axiom. We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the \({!}\)-modality of GBLL. We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of BLL using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.
For the entire collection see [Zbl 1471.68019].
For the entire collection see [Zbl 1471.68019].
References:
| [1] | Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). doi:10.1145/3408972 |
| [2] | Abramsky, S., Lenisa, M.: Linear realizability and full completeness for typed lambda-calculi. Ann. Pure Appl. Log. 134(2-3), 122-168 (2005). doi:10.1016/j.apal.2004.08.003 · Zbl 1064.03012 |
| [3] | de Amorim, A.A., Gaboardi, M., Hsu, J., Katsumata, S., Cherigui, I.: A semantic account of metric preservation. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 545-556. ACM (2017). doi:10.1145/3009837, http://dl.acm.org/citation.cfm?id=3009890 · Zbl 1380.68263 |
| [4] | Atkey, R.: Syntax and semantics of quantitative type theory. In: Dawar, A.,Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposiumon Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 56-65. ACM (2018). doi:10.1145/3209108.3209189 · Zbl 1452.03029 |
| [5] | Breuvart, F.: Dissecting Denotational Semantics: From the Well-established \(\,\, \cal{H}^*\) to the More Recent Quantitative Coeffects. Ph.D. thesis, Université Paris Diderot (2015), https://lipn.univ-paris13.fr/ breuvart/These_breuvart.pdf |
| [6] | Breuvart, F., Pagani, M.: Modelling coeffects in the relational semantics of linear logic. In: Kreutzer [23], pp. 567-581, http://www.dagstuhl.de/dagpub/978-3-939897-90-3 · Zbl 1373.03127 |
| [7] | Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 351-370. Springer Berlin Heidelberg, Berlin, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_19 · Zbl 1405.68074 |
| [8] | Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics in multiplicative-additive linear logic. Ann. Pure Appl. Log. 102(3), 247-282 (2000). doi:10.1016/S0168-0072(99)00040-8 · Zbl 0949.03057 |
| [9] | Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109(3), 205 -241 (2001). doi:10.1016/S0168-0072(00)00056-7, http://www.sciencedirect.com/science/article/pii/S0168007200000567 · Zbl 1004.03051 |
| [10] | Dal Lago, U., Hofmann, M.: Bounded linear logic, revisited. In: Curien, P.L.(ed.) Typed Lambda Calculi and Applications. pp. 80-94. Springer Berlin Heidelberg, Berlin, Heidelberg (2009). doi:10.1007/978-3-642-02273-9_8 · Zbl 1165.03001 |
| [11] | Fujii, S., Katsumata, S., Melliès, P.: Towards a formal theory of graded monads. In: Jacobs, B., Löding, C. (eds.) Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9634, pp. 513-530. Springer (2016). doi:10.1007/978-3-662-49630-5_30 · Zbl 1474.18011 |
| [12] | Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. pp. 357-370. ACM (2013). doi:10.1145/2429069.2429113, http://dl.acm.org/citation.cfm?id=2429069 · Zbl 1301.68111 |
| [13] | Gaboardi, M., Katsumata, S., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. SIGPLAN Not. 51(9), 476-489 (Sep 2016). doi:10.1145/3022670.2951939 · Zbl 1361.68037 |
| [14] | Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 331-350. SpringerBerlin Heidelberg, Berlin, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_18 · Zbl 1405.68059 |
| [15] | Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1-102 (1987). doi:10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 |
| [16] | Girard, J., Scedrov, A., Scott, P.J.: Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci. 97(1), 1-66 (1992). doi:10.1016/0304-3975(92)90386-T · Zbl 0788.03005 |
| [17] | Grellois, C., Melliès, P.: An infinitary model of linear logic. In:Pitts, A.M. (ed.) Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science,vol. 9034, pp. 41-55. Springer (2015). doi:10.1007/978-3-662-46678-0_3 · Zbl 1459.03025 |
| [18] | Grellois, C., Melliès, P.: Relational semantics of linear logic and higher-order model checking. In: Kreutzer [23], pp. 260-276, http://www.dagstuhl.de/dagpub/978-3-939897-90-3 · Zbl 1373.68287 |
| [19] | Hofmann, M., Scott, P.J.: Realizability models for bll-like languages. Theor. Comput. Sci. 318(1-2), 121-137 (2004). doi:10.1016/j.tcs.2003.10.019 · Zbl 1047.03049 |
| [20] | Hoshino, N.: Linear realizability. In: Duparc, J., Henzinger, T.A. (eds.) Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4646, pp. 420-434.Springer (2007). doi:10.1007/978-3-540-74915-8_32 · Zbl 1179.03068 |
| [21] | Hyland, M., Power, J.: Pseudo-commutative monads and pseudo-closed 2-categories. Journal of Pure and Applied Algebra 175(1), 141 - 185 (2002). doi:10.1016/S0022-4049(02)00133-0, http://www.sciencedirect.com/science/article/pii/S0022404902001330,special Volume celebrating the 70th birthday of Professor Max Kelly · Zbl 1009.18003 |
| [22] | Katsumata, S.: A double category theoretic analysis of graded linear exponential comonads. In: Baier, C., Dal Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 110-127. Springer International Publishing, Cham (2018). doi:10.1007/978-3-319-89366-2_6 · Zbl 1505.18010 |
| [23] | Kreutzer, S. (ed.): 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, LIPIcs, vol. 41. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015), http://www.dagstuhl.de/dagpub/978-3-939897-90-3 · Zbl 1329.68032 |
| [24] | Lago, U.D., Gaboardi, M.: Linear dependent types and relative completeness. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pp. 133-142. IEEE Computer Society (2011). doi:10.1109/LICS.2011.22, https://ieeexplore.ieee.org/xpl/conhome/5968099/proceeding · Zbl 1261.03073 |
| [25] | McBride, C.: I got plenty o’ nuttin’. In: Lindley, S., McBride, C., Trinder,P.W., Sannella, D. (eds.) A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 9600, pp. 207-233. Springer (2016). doi:10.1007/978-3-319-30936-1_12 · Zbl 1333.68014 |
| [26] | Orchard, D., Liepelt, V.B., Eades III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). doi:10.1145/3341714 |
| [27] | Orchard, D., Wadler, P., Eades, H.: Unifying graded and parameterised monads. Electronic Proceedings in Theoretical Computer Science 317, 18-38 (May 2020). doi:10.4204/eptcs.317.2 · Zbl 1511.68056 |
| [28] | Petricek, T., Orchard, D., Mycroft, A.: Coeffects: Unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) Automata, Languages, and Programming. pp. 385-397. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). doi:10.1007/978-3-642-39212-2_35 · Zbl 1334.68049 |
| [29] | Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. pp. 157-168. ACM (2010). doi:10.1145/1863543.1863568 · Zbl 1323.68254 |
| [30] | Schöpp, U.: Computation-by-interaction with effects. In: Yang, H. (ed.)Programming Languages and Systems. pp. 305-321. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). doi:10.1007/978-3-642-25318-8_23 |
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.
