Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). https://doi.org/10.1145/3408972
Abramsky, S., Lenisa, M.: Linear realizability and full completeness for typed lambda-calculi. Ann. Pure Appl. Log. 134(2-3), 122–168 (2005). https://doi.org/10.1016/j.apal.2004.08.003
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). https://doi.org/10.1145/3009837, http://dl.acm.org/citation.cfm?id=3009890
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). https://doi.org/10.1145/3209108.3209189
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
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
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). https://doi.org/10.1007/978-3-642-54833-8_19
Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics in multiplicative-additive linear logic. Ann. Pure Appl. Log. 102(3), 247–282 (2000). https://doi.org/10.1016/S0168-0072(99)00040-8
Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109(3), 205 –241 (2001). https://doi.org/10.1016/S0168-0072(00)00056-7, http://www.sciencedirect.com/science/article/pii/S0168007200000567
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). https://doi.org/10.1007/978-3-642-02273-9_8
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). https://doi.org/10.1007/978-3-662-49630-5_30
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). https://doi.org/10.1145/2429069.2429113, http://dl.acm.org/citation.cfm?id=2429069
Gaboardi, M., Katsumata, S., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. SIGPLAN Not. 51(9), 476–489 (Sep 2016). https://doi.org/10.1145/3022670.2951939
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). https://doi.org/10.1007/978-3-642-54833-8_18
Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4
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). https://doi.org/10.1016/0304-3975(92)90386-T
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). https://doi.org/10.1007/978-3-662-46678-0_3
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
Hofmann, M., Scott, P.J.: Realizability models for bll-like languages. Theor. Comput. Sci. 318(1-2), 121–137 (2004). https://doi.org/10.1016/j.tcs.2003.10.019
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). https://doi.org/10.1007/978-3-540-74915-8_32
Hyland, M., Power, J.: Pseudo-commutative monads and pseudo-closed 2-categories. Journal of Pure and Applied Algebra 175(1), 141 – 185 (2002). https://doi.org/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
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). https://doi.org/10.1007/978-3-319-89366-2_6
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
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). https://doi.org/10.1109/LICS.2011.22, https://ieeexplore.ieee.org/xpl/conhome/5968099/proceeding
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). https://doi.org/10.1007/978-3-319-30936-1_12
Orchard, D., Liepelt, V.B., Eades III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https://doi.org/10.1145/3341714
Orchard, D., Wadler, P., Eades, H.: Unifying graded and parameterised monads. Electronic Proceedings in Theoretical Computer Science 317, 18–38 (May 2020). https://doi.org/10.4204/eptcs.317.2
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). https://doi.org/10.1007/978-3-642-39212-2_35
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). https://doi.org/10.1145/1863543.1863568
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). https://doi.org/10.1007/978-3-642-25318-8_23
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Fukihara, Y., Katsumata, Sy. (2021). Generalized Bounded Linear Logic and its Categorical Semantics. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)