×

Bisimulations for delimited-control operators. (English) Zbl 1421.68012

Summary: We present a comprehensive study of the behavioral theory of an untyped \(\lambda\)-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and environmental) within a unifying framework, and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.

MSC:

68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: arXiv

References:

[1] S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105:159-267, 1993. · Zbl 0779.03003
[2] Z. M. Ariola, H. Herbelin, and A. Sabry. A proof-theoretic foundation of abortive continuations. HigherOrder and Symbolic Computation, 20(4):403-429, 2007. · Zbl 1128.68089
[3] A. Aristiz´abal, D. Biernacki, S. Lenglet, and P. Polesiuk. Environmental Bisimulations for DelimitedControl Operators with Dynamic Prompt Generation. Logical Methods in Computer Science, 13(3), 2017. · Zbl 1421.68009
[4] K. Asai. Logical relations for call-by-value delimited continuations. In M. van Eekelen, editor, Proceedings of the Sixth Symposium on Trends in Functional Programming (TFP 2005), pages 413-428, Tallinn, Estonia, Sept. 2005. Institute of Cybernetics at Tallinn Technical University. Extended version available as Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 06-1.
[5] K. Asai and Y. Kameyama. Polymorphic delimited continuations. In Shao [86], pages 239-254. · Zbl 1137.68344
[6] M. Biernacka and D. Biernacki. Context-based proofs of termination for typed delimited-control operators. In F. J. L´opez-Fraguas, editor, PPDP’09, Coimbra, Portugal, Sept. 2009. ACM Press. · Zbl 1337.68061
[7] M. Biernacka, D. Biernacki, and O. Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1-39, Nov. 2005. · Zbl 1125.68050
[8] M. Biernacka, D. Biernacki, and S. Lenglet. Typing control operators in the CPS hierarchy. In M. Hanus, editor, Proceedings of the 13th ACM-SIGPLAN International Conference on Principles and Practice of
[9] M. Biernacka, D. Biernacki, S. Lenglet, and M. Materzok. Proving termination of evaluation for system F with control operators. In U. de’Liguoro and A. Saurin, editors, Proceedings of the 1st Workshop on Control Operators and their Semantics (COS 2013), volume 127 of Electronic Proceedings in Theoretical Computer Science, pages 15-27, Eindhoven, The Netherlands, June 2013. · Zbl 1471.68055
[10] D. Biernacki and O. Danvy. A simple proof of a folklore theorem about delimited control. Journal of Functional Programming, 16(3):269-280, 2006. · Zbl 1092.68021
[11] D. Biernacki, O. Danvy, and K. Millikin. A dynamic continuation-passing style for dynamic delimited continuations. ACM Trans. Program. Lang. Syst., 38(1):2:1-2:25, 2015.
[12] D. Biernacki, O. Danvy, and C. Shan. On the static and dynamic extents of delimited continuations. Science of Computer Programming, 60(3):274-297, 2006. · Zbl 1101.68442
[13] D. Biernacki and S. Lenglet. Applicative bisimulations for delimited-control operators. In L. Birkedal, editor, FOSSACS’12, number 7213 in LNCS, pages 119-134, Tallinn, Estonia, Mar. 2012. Springer-Verlag. · Zbl 1352.68037
[14] D. Biernacki and S. Lenglet. Normal form bisimulations for delimited-control operators. In T. Schrijvers and P. Thiemann, editors, FLOPS’12, number 7294 in LNCS, pages 47-61, Kobe, Japan, May 2012. Springer-Verlag. · Zbl 1354.68044
[15] D. Biernacki and S. Lenglet. Environmental bisimulations for delimited-control operators. In C. Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, 2013. Proceedings, volume 8301 of Lecture Notes in Computer Science, pages 333-348, Melbourne, VIC, Australia, Dec. 2013. Springer. · Zbl 1421.68010
[16] D. Biernacki and S. Lenglet. Applicative bisimilarities for call-by-name and call-by-value λµ-calculus. In B. Jacobs, A. Silva, and S. Staton, editors, Proceedings of the 30th Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXX), volume 308 of Electronic Notes in Theoretical Computer Science, pages 49-64, Ithaca, USA, June 2014. · Zbl 1337.68056
[17] D. Biernacki, S. Lenglet, and P. Polesiuk. Proving soundness of extensional normal-form bisimilarities. In A. Silva, editor, Proceedings of the 33th Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXXIII), volume 336 of Electronic Notes in Theoretical Computer Science, pages 41-56, Ljubljana, Slovenia, June 2017. · Zbl 1421.68011
[18] T. Crolard. A confluent lambda-calculus with a catch/throw mechanism. JFP, 9(6):625-647, 1999. · Zbl 0954.68039
[19] O. Danvy. Type-directed partial evaluation. In Steele Jr. [87], pages 242-257.
[20] O. Danvy and A. Filinski. A functional abstraction of typed contexts. DIKU Rapport 89/12, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, July 1989.
[21] O. Danvy and A. Filinski. Abstracting control. In M. Wand, editor, LFP’90, pages 151-160, Nice, France, June 1990. ACM Press.
[22] P. Downen and Z. M. Ariola. A systematic approach to delimited control with multiple prompts. In H. Seidl, editor, Programming Languages and Systems, 21st European Symposium on Programming, ESOP 2012, Lecture Notes in Computer Science, pages 234-253, Tallinn, Estonia, Mar. 2012. Springer-Verlag. · Zbl 1352.68041
[23] D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5):477-528, 2012. · Zbl 1252.68187
[24] P. Dybjer and A. Filinski. Normalization and partial evaluation. In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors, Applied Semantics - Advanced Lectures, number 2395 in Lecture Notes in Computer Science, pages 137-192, Caminha, Portugal, Sept. 2000. Springer-Verlag. · Zbl 1065.68026
[25] R. K. Dybvig, S. Peyton-Jones, and A. Sabry. A monadic framework for delimited continuations. Journal of Functional Programming, 17(6):687-730, 2007. · Zbl 1130.68038
[26] M. Felleisen. The theory and practice of first-class prompts. In J. Ferrante and P. Mager, editors, POPL’88, pages 180-190, San Diego, California, Jan. 1988. ACM Press.
[27] A. Filinski. Representing monads. In H.-J. Boehm, editor, POPL’94, pages 446-457, Portland, Oregon, Jan. 1994. ACM Press.
[28] A. Filinski. Representing layered monads. In A. Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 175-188, San Antonio, Texas, Jan. 1999. ACM Press.
[29] M. Flatt, G. Yu, R. B. Findler, and M. Felleisen. Adding delimited and composable control to a production programming environment. In N. Ramsey, editor, Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP’07), SIGPLAN Notices, Vol. 42, No. 9,
[30] A. D. Gordon. Bisimilarity as a theory of functional programming. Theoretical Computer Science, 228(1-2):5-47, 1999. · Zbl 0968.68028
[31] A. D. Gordon and G. D. Rees. Bisimilarity for a first-order calculus of objects with subtyping. In Steele Jr. [87], pages 386-395.
[32] C. Gunter, D. R´emy, and J. G. Riecke. A generalization of exceptions and control in ML-like languages. In S. Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 12-23, La Jolla, California, June 1995. ACM Press.
[33] H. Herbelin and S. Ghilezan. An approach to call-by-name delimited continuations. In P. Wadler, editor, Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 383-394. ACM Press, Jan. 2008. · Zbl 1295.68063
[34] R. Hieb, R. K. Dybvig, and C. W. Anderson, III. Subcontinuations. Lisp and Symbolic Computation, 5(4):295-326, Dec. 1993.
[35] D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103-112, 1996. · Zbl 0853.68073
[36] C. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In J. Field and M. Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 59-72. ACM, 2012. · Zbl 1321.68198
[37] C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. A logical step forward in parametric bisimulations. Technical Report MPI-SWS-2014-003, Max Planck Institute for Software Systems (MPI-SWS), Saarbrcken, Germany, Jan. 2014.
[38] Y. Kameyama. Axioms for control operators in the CPS hierarchy. Higher-Order and Symbolic Computation, 20(4):339-369, 2007. · Zbl 1128.68009
[39] Y. Kameyama and M. Hasegawa. A sound and complete axiomatization of delimited continuations. In O. Shivers, editor, ICFP’03, SIGPLAN Notices, Vol. 38, No. 9, pages 177-188, Uppsala, Sweden, Aug. 2003. ACM Press. · Zbl 1315.68098
[40] Y. Kameyama and A. Tanaka. Equational axiomatization of call-by-name delimited control. In T. Kutsia, W. Schreiner, and M. Fern´andez, editors, Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming,, pages 77-86, Hagenberg, Austria, July 2010. ACM.
[41] O. Kiselyov. How to remove a dynamic prompt: Static and dynamic delimited continuation operators are equally expressible. Technical Report 611, Computer Science Department, Indiana University, Bloomington, Indiana, Mar. 2005.
[42] O. Kiselyov. Delimited control in OCaml, abstractly and concretely: System description. In M. Blume and G. Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, number 6009 in Lecture Notes in Computer Science, pages 304-320, Sendai, Japan, Apr. 2010. Springer.
[43] O. Kiselyov and C. Shan. Delimited continuations in operating systems. In B. Kokinov, D. C. Richardson, T. R. Roth-Berghofer, and L. Vieu, editors, Modeling and Using Context, 6th International and Interdisciplinary Conference, CONTEXT 2007, number 4635 in Lecture Notes in Artificial Intelligence, pages 291-302, Roskilde, Denmark, Aug. 2007. Springer.
[44] O. Kiselyov and C. Shan. Embedded probabilistic programming. In W. Taha, editor, Domain-Specific Languages, DSL 2009, number 5658 in Lecture Notes in Computer Science, pages 360-384, Oxford, UK, July 2009. Springer.
[45] O. Kiselyov, C. Shan, D. P. Friedman, and A. Sabry. Backtracking, interleaving, and terminating monad transformers. In B. Pierce, editor, Proceedings of the 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP’05), SIGPLAN Notices, Vol. 40, No. 9, pages 192-203, Tallinn, Estonia, Sept. 2005. ACM Press. · Zbl 1302.68061
[46] V. Koutavas, P. B. Levy, and E. Sumii. From applicative to environmental bisimulation. In M. Mislove and J. Ouaknine, editors, Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXVII), volume 276 of ENTCS, pages 215-235, Pittsburgh, PA, USA, May 2011. · Zbl 1342.68089
[47] V. Koutavas and M. Wand. Bisimulations for untyped imperative objects. In P. Sestoft, editor, ESOP’06, volume 3924 of Lecture Notes in Computer Science, pages 146-161, Vienna, Austria, Mar. 2006. Springer. · Zbl 1178.68154
[48] V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In J. G. Morrisett and S. L. P. Jones, editors, POPL’06, pages 141-152, Charleston, SC, USA, Jan. 2006. ACM Press. · Zbl 1370.68048
[49] J. Krivine. Classical logic, storage operators and second-order lambda-calculus. Annals of Pure and Applied Logic, 68(1):53-78, 1994. · Zbl 0814.03009
[50] I. Lanese, J. A. P´erez, D. Sangiorgi, and A. Schmitt. On the expressiveness and decidability of higher-order process calculi. Inf. Comput., 209(2):198-226, 2011. · Zbl 1238.68100
[51] S. B. Lassen. Bisimulation for pure untyped λµ-caluclus (extended abstract). Unpublished note, Jan. 1999.
[52] S. B. Lassen. Bisimulation in untyped lambda calculus: B¨ohm trees and bisimulation up to context. In M. M. Stephen Brookes, Achim Jung and A. Scedrov, editors, MFPS’99, volume 20 of ENTCS, pages 346-374, New Orleans, LA, Apr. 1999. Elsevier Science. · Zbl 0924.68030
[53] S. B. Lassen. Eager normal form bisimulation. In P. Panangaden, editor, LICS’05, pages 345-354, Chicago, IL, June 2005. IEEE Computer Society Press.
[54] S. B. Lassen. Normal form simulation for McCarthy’s amb. In M. Escard´o, A. Jung, and M. Mislove, editors, MFPS’05, volume 155 of ENTCS, pages 445-465, Birmingham, UK, May 2005. Elsevier Science Publishers. · Zbl 1273.68088
[55] S. B. Lassen. Head normal form bisimulation for pairs and the λµ-calculus. In R. Alur, editor, LICS’06, pages 297-306, Seattle, WA, Aug. 2006. IEEE Computer Society Press.
[56] S. B. Lassen and P. B. Levy. Typed normal form bisimulation. In J. Duparc and T. A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 283-297, Lausanne, Switzerland, Sept. 2007. Springer. · Zbl 1179.68038
[57] S. B. Lassen and P. B. Levy. Typed normal form bisimulation for parametric polymorphism. In F. Pfenning, editor, LICS’08, pages 341-352, Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society Press.
[58] J. L. Lawall and O. Danvy. Continuation-based partial evaluation. In C. L. Talcott, editor, Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3, pages 227-238, Orlando, Florida, June 1994. ACM Press.
[59] S. Lenglet, A. Schmitt, and J.-B. Stefani. Howe’s method for calculi with passivation. In M. Bravetti and G. Zavattaro, editors, CONCUR’09, number 5710 in LNCS, pages 448-462, Bologna, Italy, July 2009. Springer. · Zbl 1254.68174
[60] J. Madiot, D. Pous, and D. Sangiorgi. Bisimulations up-to: Beyond first-order transition systems. In P. Baldan and D. Gorla, editors, 25th International Conference on Concurrency Theory, volume 8704 of Lecture Notes in Computer Science, pages 93-108, Rome, Italy, Sept. 2014. Springer. · Zbl 1388.68200
[61] J.-M. Madiot. Higher-order languages: dualities and bisimulation enhancements. PhD thesis, Universit´e de Lyon and Universit‘a di Bologna, 2015.
[62] M. Materzok. Axiomatizing subtyped delimited continuations. In S. R. D. Rocca, editor, Computer Science Logic 2013, CSL 2013, volume 23 of LIPIcs, pages 521-539, Torino, Italy, Sept. 2013. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. · Zbl 1356.68036
[63] M. Materzok and D. Biernacki. Subtyping delimited continuations. In O. Danvy, editor, Proceedings of the 2011 ACM SIGPLAN International Conference on Functional Programming (ICFP’11), pages 81-93, Tokyo, Japan, Sept. 2011. ACM Press. · Zbl 1323.68081
[64] M. Merro. On the observational theory of the CPS-calculus. Acta Informatica, 47(2):111-132, 2010. · Zbl 1211.68270
[65] R. Milner. Fully abstract models of typed λ-calculi. Theoretical Computer Science, 4(1):1-22, 1977. · Zbl 0386.03006
[66] L. Moreau and C. Queinnec. Partial continuations as the difference of continuations, a duumvirate of control operators. In M. Hermenegildo and J. Penjam, editors, Sixth International Symposium on Programming Language Implementation and Logic Programming, number 844 in Lecture Notes in Computer Science, pages 182-197, Madrid, Spain, Sept. 1994. Springer-Verlag.
[67] J. H. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, Massachusets Institute of Technology, 1968.
[68] M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, LPAR’92, number 624 in LNAI, pages 190-201, St. Petersburg, Russia, July 1992. Springer-Verlag. · Zbl 0925.03092
[69] A. Pitts and I. Stark. Operational reasoning for functions with local state. In A. Gordon and A. Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227-273. Publications of the Newton Institute, Cambridge University Press, 1998. · Zbl 0967.68035
[70] A. M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10(3):321-359, 2000. · Zbl 0955.68024
[71] G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975. · Zbl 0325.68006
[72] D. Pous. Complete lattices and up-to techniques. In Shao [86], pages 351-366. · Zbl 1138.68041
[73] D. Pous. Coinduction all the way up. In M. Grohe, E. Koskinen, and N. Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, pages 307-316, New York, NY, USA, July 2016. ACM. · Zbl 1394.68352
[74] D. Pous and D. Sangiorgi. Enhancements of the bisimulation proof method. In D. Sangiorgi and J. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, chapter 6, pages 233-289. Cambridge University Press, 2011. · Zbl 1285.68111
[75] T. Rompf, I. Maier, and M. Odersky. Implementing first-class polymorphic delimited continuations by a type-directed selective cps-transform. In A. Tolmach, editor, Proceedings of the 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP’09), pages 317-328, Edinburgh, UK, Aug. 2009. ACM Press. · Zbl 1302.68187
[76] A. Sabry. Note on axiomatizing the semantics of control operators. Technical Report CIS-TR-96-03, Department of Computer and Information Science, University of Oregon, 1996.
[77] D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. In A. Scedrov, editor, LICS’92, pages 102-109, Santa Cruz, California, June 1992. IEEE Computer Society.
[78] D. Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447- 479, Oct. 1998. · Zbl 0916.68057
[79] D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. In J. Marcinkowski, editor, LICS’07, pages 293-302, Wroclaw, Poland, July 2007. IEEE Computer Society Press.
[80] D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1):1-69, Jan. 2011.
[81] D. Sangiorgi and D. Walker. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. · Zbl 0981.68116
[82] N. Sato and E. Sumii. The higher-order, call-by-value applied Pi-calculus. In Z. Hu, editor, APLAS’09, volume 5904 of LNCS, pages 311-326, Seoul, Korea, Dec. 2009. Springer-Verlag.
[83] C. Shan. Delimited continuations in natural language: quantification and polarity sensitivity. In H. Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW’04), Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pages 55-64, Venice, Italy, Jan. 2004.
[84] C. Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. · Zbl 1128.68010
[85] Z. Shao, editor. Proceedings of the Fifth Asian Symposium on Programming Languages and Systems, APLAS’07, number 4807 in LNCS, Singapore, Dec. 2007. Springer-Verlag.
[86] G. L. Steele Jr., editor. Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, Jan. 1996. ACM Press.
[87] K. Støvring and S. B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In M. Felleisen, editor, POPL’07, SIGPLAN Notices, Vol. 42, No. 1, pages 161-172, Nice, France, Jan. 2007. ACM Press. · Zbl 1295.68093
[88] E. Sumii. An implementation of transparent migration on standard Scheme. In M. Felleisen, editor, Proceedings of the Workshop on Scheme and Functional Programming, Technical Report 00-368, Rice University, pages 61-64, Montr´eal, Canada, Sept. 2000.
[89] E. Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In E. Gr¨adel and R. Kahle, editors, Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Proceedings, volume 5771 of Lecture Notes in Computer Science, pages 455-469, Coimbra, Portugal, Sept. 2009. Springer. · Zbl 1257.03040
[90] E. Sumii and B. C. Pierce. A bisimulation for dynamic sealing. Theoretical Computer Science, 375(13):169-192, 2007. · Zbl 1111.68034
[91] E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5), 2007. · Zbl 1326.68073
[92] H. Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 1997. ECS-LFCS-97-376.
[93] J. Tiuryn and M. Wand. Untyped lambda-calculus with input-output. In H. Kirchner, editor, 21st Colloquium on Trees in Algebra and Programming (CAAP’96), volume 1059 of Lecture Notes in Computer Science, pages 317-329, Link¨oping, Sweden, Apr. 1996. Springer-Verlag. · Zbl 1508.68213
[94] M. Wand and D. Vaillancourt. Relating models of backtracking. In K. Fisher, editor, Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP’04), SIGPLAN Notices, Vol. 39, No. 9, pages 54-65, Snowbird, Utah, Sept. 2004. ACM Press. · Zbl 1323.68176
[95] T. Yachi and E. Sumii. A sound and complete bisimulation for contextual equivalence in \lambda -calculus with call/cc. In A. Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 171-186, 2016. · Zbl 1483.68064
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.