References

  1. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride & James McKinna (2021): A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Journal of Functional Programming 31, pp. e22, doi:10.1017/S0956796820000076.
  2. Andreas Abel & Jean-Philippe Bernardy (2020): A Unified View of Modalities in Type Systems. Proc. ACM Program. Lang. 4(ICFP), doi:10.1145/3408972.
  3. Guillaume Allais (2018): Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In: TYPES 2017, pp. 1:1–1:22, doi:10.4230/LIPIcs.TYPES.2017.1.
  4. Andrew Barber (1996): Dual Intuitionistic Linear Logic. Technical Report. University of Edinburgh.
  5. P. N. Benton, Gavin M. Bierman, Valeria de Paiva & Martin Hyland (1993): A Term Calculus for Intuitionistic Linear Logic. In: Typed Lambda Calculi and Applications, LNCS 664. Springer, pp. 75–90, doi:10.1007/BFb0037099.
  6. Aloïs Brunel, Marco Gaboardi, Damiano Mazza & Steve Zdancewic (2014): A Core Quantitative Coeffect Calculus. In: Zhong Shao: Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Lecture Notes in Computer Science 8410. Springer, pp. 351–370, doi:10.1007/978-3-642-54833-8_19.
  7. Nick Benton, Chung-Kil Hur, Andrew Kennedy & Conor McBride (2012): Strongly typed term representations in Coq. J. of Autom Reasoning 49(2), doi:10.1007/s10817-011-9219-0.
  8. Kaustuv Chaudhuri, Leonardo Lima & Giselle Reis (2019): Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci. 781, pp. 24–38, doi:10.1016/j.tcs.2019.02.023.
  9. Karl Crary (2010): Higher-Order Representation of Substructural Logics. SIGPLAN Not. 45(9), pp. 131142, doi:10.1145/1932681.1863565.
  10. Dan R. Ghica & Alex I. Smith (2014): Bounded Linear Types in a Resource Semiring. In: Zhong Shao: Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Lecture Notes in Computer Science 8410. Springer, pp. 331–350, doi:10.1007/978-3-642-54833-8_18.
  11. Olivier Laurent (2018): Preliminary Report on the Yalla Library. Available at https://perso.ens-lyon.fr/olivier.laurent/yalla/. Coq Workshop.
  12. Daniel R. Licata, Michael Shulman & Mitchell Riley (2017): A Fibrational Framework for Substructural and Modal Logics. In: FSCD 2017, pp. 25:1–25:22, doi:10.4230/LIPIcs.FSCD.2017.25.
  13. Conor McBride (2005): Type-preserving renaming and substitution. Available at http://www.strictlypositive.org/ren-sub.pdf.
  14. Dominic Orchard, Vilem-Benjamin Liepelt & Harley Eades III (2019): Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP), pp. 110:1–110:30, doi:10.1145/3341714.
  15. Frank Pfenning & Rowan Davies (2001): A judgmental reconstruction of modal logic 11, pp. 511–540, doi:10.1017/S0960129501003322.
  16. Tomas Petricek, Dominic A. Orchard & Alan Mycroft (2014): Coeffects: a calculus of context-dependent computation. In: Johan Jeuring & Manuel M. T. Chakravarty: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. ACM, pp. 123–135, doi:10.1145/2628136.2628160.
  17. James Power & Caroline Webster (1999): Working with Linear Logic in Coq. 12th International Conference on Theorem Proving in Higher Order Logics (Work-in-progress paper).
  18. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers & Eelco Visser (2020): Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In: CPP 2020, pp. 284–298, doi:10.1145/3372885.3373818.
  19. Jason Reed & Benjamin C. Pierce (2010): Distance makes the types grow stronger: a calculus for differential privacy. In: Paul Hudak & Stephanie Weirich: Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. ACM, pp. 157–168, doi:10.1145/1863543.1863568.
  20. Kornél Szlachányi (2012): Skew-monoidal categories and bialgebroids. Advances in Mathematics 231(3-4), pp. 1694–1730, doi:10.1016/j.aim.2012.06.027.
  21. Philip Wadler (1992): There's no substitute for linear logic. In: 8th International Workshop on the Mathematical Foundations of Programming Semantics.
  22. Bruno Xavier, Carlos Olarte, Giselle Reis & Vivek Nigam (2017): Mechanizing Focused Linear Logic in Coq. In: 12th Workshop on Logical and Semantic Frameworks, with Applications, ENTCS 338. Elsevier, pp. 219–236, doi:10.1016/j.entcs.2018.10.014.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org