{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T07:14:49Z","timestamp":1780384489612,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030411022","type":"print"},{"value":"9783030411039","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-41103-9_4","type":"book-chapter","created":{"date-parts":[[2020,2,14]],"date-time":"2020-02-14T10:04:59Z","timestamp":1581674699000},"page":"105-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Galois Connections for Recursive Types"],"prefix":"10.1007","author":[{"given":"Ahmad Salim","family":"Al-Sibahi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,2,15]]},"reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2005.06.002","volume":"342","author":"MG Abbott","year":"2005","unstructured":"Abbott, M.G., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theoret. Comput. Sci. 342(1), 3\u201327 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR2","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"S Abramsky","year":"1994","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1\u2013168. Clarendon Press, Oxford (1994)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3540543961_21","volume-title":"Functional Programming Languages and Computer Architecture","author":"A Aiken","year":"1991","unstructured":"Aiken, A., Murphy, B.R.: Implementing regular tree expressions. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 427\u2013447. Springer, Heidelberg (1991). \nhttps:\/\/doi.org\/10.1007\/3540543961_21"},{"key":"4_CR4","volume-title":"Category Theory","author":"S Awodey","year":"2011","unstructured":"Awodey, S.: Category Theory. Oxford University Press, Oxford (2011)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-57264-3_42","volume-title":"Static Analysis","author":"PN Benton","year":"1993","unstructured":"Benton, P.N.: Strictness properties of lazy algebraic datatypes. In: Cousot, P., Falaschi, M., Fil\u00e9, G., Rauzy, A. (eds.) WSA 1993. LNCS, vol. 724, pp. 206\u2013217. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/3-540-57264-3_42"},{"issue":"POPL","key":"4_CR6","first-page":"44:1","volume":"3","author":"M Bodin","year":"2019","unstructured":"Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their interpretations. PACMPL 3(POPL), 44:1\u201344:31 (2019)","journal-title":"PACMPL"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Relational inductive shape analysis. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74061-2_24"},{"key":"4_CR9","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR11","unstructured":"Cousot, P., Cousot, R.: Invited talk: higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis. In: Bal, H.E. (ed.) Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages, Toulouse, France, 16\u201319 May 1994, pp. 95\u2013112. IEEE Computer Society (1994)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA 1995, pp. 170\u2013181. ACM (1995)","DOI":"10.1145\/224164.224199"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-45937-5_13","volume-title":"Compiler Construction","author":"P Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159\u2013179. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45937-5_13"},{"issue":"ICFP","key":"4_CR14","first-page":"12:1","volume":"1","author":"D Darais","year":"2017","unstructured":"Darais, D., Labich, N., Nguyen, P.C., Horn, D.V.: Abstracting definitional interpreters (functional pearl). PACMPL 1(ICFP), 12:1\u201312:25 (2017)","journal-title":"PACMPL"},{"issue":"5","key":"4_CR15","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1145\/265943.265966","volume":"19","author":"TP Jensen","year":"1997","unstructured":"Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst. 19(5), 751\u2013803 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-99725-4_16","volume-title":"Static Analysis","author":"M Journault","year":"2018","unstructured":"Journault, M., Min\u00e9, A., Ouadjaout, A.: Modular static analysis of string manipulations in C programs. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 243\u2013262. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-99725-4_16"},{"issue":"ICFP","key":"4_CR17","first-page":"72:1","volume":"2","author":"S Keidel","year":"2018","unstructured":"Keidel, S., Poulsen, C.B., Erdweg, S.: Compositional soundness proofs of abstract interpreters. PACMPL 2(ICFP), 72:1\u201372:26 (2018)","journal-title":"PACMPL"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-69166-2_23","volume-title":"Static Analysis","author":"J Midtgaard","year":"2008","unstructured":"Midtgaard, J., Jensen, T.: A calculational approach to control-flow analysis by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 347\u2013362. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69166-2_23"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1016\/0167-6423(94)00009-3","volume":"22","author":"F Nielson","year":"1994","unstructured":"Nielson, F., Nielson, H.R.: The tensor product in wadler\u2019s analysis of lists. Sci. Comput. Program. 22(3), 327\u2013354 (1994)","journal-title":"Sci. Comput. Program."},{"key":"4_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-04652-0_5"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/978-3-662-45231-8_40","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"X Rival","year":"2014","unstructured":"Rival, X., Toubhans, A., Chang, B.-Y.E.: Construction of abstract domains for heterogeneous properties (position paper). In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 489\u2013492. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-45231-8_40"},{"key":"4_CR23","doi-asserted-by":"publisher","DOI":"10.1142\/6284","volume-title":"Domain-Theoretic Foundations of Functional Programming","author":"T Streicher","year":"2006","unstructured":"Streicher, T.: Domain-Theoretic Foundations of Functional Programming. World Scientific Publishing Company, Singapore (2006)"},{"issue":"2","key":"4_CR24","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375\u2013395. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35873-9_23"}],"container-title":["Lecture Notes in Computer Science","From Lambda Calculus to Cybersecurity Through Program Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41103-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,14]],"date-time":"2020-02-14T19:07:38Z","timestamp":1581707258000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41103-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030411022","9783030411039"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41103-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"15 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}