{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T22:40:02Z","timestamp":1754174402407,"version":"3.41.2"},"publisher-location":"Cham","reference-count":203,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030817008"},{"type":"electronic","value":"9783030817015"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-81701-5_3","type":"book-chapter","created":{"date-parts":[[2021,8,3]],"date-time":"2021-08-03T15:16:19Z","timestamp":1628003779000},"page":"59-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Algorithmics"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bird","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Gibbons","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Hinze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johan","family":"Jeuring","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lambert","family":"Meertens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"M\u00f6ller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Schrijvers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,4]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(94)00195-5","volume":"53","author":"C Aarts","year":"1995","unstructured":"Aarts, C., et al.: Fixed-point calculus. Inf. Process. Lett. 53(3), 131\u2013136 (1995)","journal-title":"Inf. Process. Lett."},{"key":"3_CR2","unstructured":"Agresti, W.M.: What are the new paradigms? In: Agresti, W.M. (ed.) New Paradigms for Software Development. IEEE Computer Society Press (1986)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.scico.2017.04.003","volume":"164","author":"J Alpuim","year":"2018","unstructured":"Alpuim, J., Swierstra, W.: Embedding the refinement calculus in Coq. Sci. Comput. Program. 164, 37\u201348 (2018)","journal-title":"Sci. Comput. Program."},{"key":"3_CR4","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-0-387-35672-3_1","volume-title":"Generic Programming","author":"T Altenkirch","year":"2003","unstructured":"Altenkirch, T., Mcbride, C.: Generic programming within dependently typed programming. In: Gibbons, J., Jeuring, J. (eds.) Generic Programming. ITIFIP, vol. 115, pp. 1\u201320. Springer, Boston, MA (2003). https:\/\/doi.org\/10.1007\/978-0-387-35672-3_1"},{"key":"3_CR5","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Kleene_Algebra.html"},{"key":"3_CR6","unstructured":"Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs (2014). http:\/\/isa-afp.org\/entries\/Relation_Algebra.html"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne - a language with dependent types. In: International Conference on Functional Programming, ICFP 1998, pp. 239\u2013250 (1998)","DOI":"10.1145\/289423.289451"},{"key":"3_CR8","unstructured":"Back, R.J.: On the correctness of refinement steps in program development. PhD thesis. Report A-1978-4, Department of Computer Science, University of Helsinki (1978)"},{"issue":"1","key":"3_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"RJ Back","year":"1981","unstructured":"Back, R.J.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49\u201368 (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90005-2","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, Springer (1998). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2_4","DOI":"10.1007\/978-1-4612-1674-2_4"},{"key":"3_CR11","unstructured":"Backhouse, R.: An exploration of the Bird-Meertens formalism. Technical report CS 8810, Department of Computer Science, Groningen University (1988)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Backhouse, R., Michaelis, D.: Fixed-point characterisation of winning strategies in impartial games. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. Lecture Notes in Computer Science, vol. 3051, pp. 34\u201347. Springer (2004)","DOI":"10.1007\/978-3-540-24771-5_4"},{"issue":"1","key":"3_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BF01887198","volume":"1","author":"R Backhouse","year":"1989","unstructured":"Backhouse, R., Chisholm, P., Malcolm, G., Saaman, E.: Do-it-yourself type theory. Formal Aspects Comput. 1(1), 19\u201384 (1989)","journal-title":"Formal Aspects Comput."},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.): Spring School on Datatype-Generic Programming, Lecture Notes in Computer Science, vol. 4719. Springer-Verlag (2007). https:\/\/doi.org\/10.1007\/978-3-540-76786-2","DOI":"10.1007\/978-3-540-76786-2"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1093\/imamat\/15.2.161","volume":"15","author":"RC Backhouse","year":"1975","unstructured":"Backhouse, R.C., Carr\u00e9, B.A.: Regular algebra applied to path-finding problems. IMA J. Appl. Math. 15(2), 161\u2013186 (1975). https:\/\/doi.org\/10.1093\/imamat\/15.2.161","journal-title":"IMA J. Appl. Math."},{"issue":"3\u20134","key":"3_CR16","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/s00224-007-9056-z","volume":"43","author":"RC Backhouse","year":"2008","unstructured":"Backhouse, R.C., Doornbos, H.: Datatype-generic termination proofs. Theor. Comput. Syst. 43(3\u20134), 362\u2013393 (2008). https:\/\/doi.org\/10.1007\/s00224-007-9056-z","journal-title":"Theor. Comput. Syst."},{"issue":"11","key":"3_CR17","doi-asserted-by":"publisher","first-page":"2029","DOI":"10.1016\/j.scico.2012.07.007","volume":"78","author":"RC Backhouse","year":"2013","unstructured":"Backhouse, R.C., Chen, W., Ferreira, J.F.: The algorithmics of solitaire-like games. Sci. Comput. Program. 78(11), 2029\u20132046 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.07.007","journal-title":"Sci. Comput. Program."},{"key":"3_CR18","unstructured":"Backhouse, R.C., Doornbos, H., Gl\u00fcck, R., van der Woude, J.: Elements of algorithmic graph theory: an exercise in point-free reasoning, (working document) (2019)"},{"key":"3_CR19","unstructured":"Balzer, R., Goldman, N., Wile, D.: On the transformational implementation approach to programming. In: Yeh, R.T., Ramamoorthy, C.V. (eds.) International Conference on Software Engineering, IEEE Computer Society, pp. 337\u2013344 (1976)"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Batory, D.S., H\u00f6fner, P., Kim, J.: Feature interactions, products, and composition. In: Denney, E., Schultz, U.P. (eds.) Generative Programming and Component Engineering. ACM, pp. 13\u201322 (2011). https:\/\/doi.org\/10.1145\/2047862.2047867","DOI":"10.1145\/2047862.2047867"},{"key":"3_CR21","unstructured":"Bauer, F.L.: Programming as an evolutionary process. In: Yeh, R.T., Ramamoorthy, C. (eds.) International Conference on Software Engineering, IEEE Computer Society, pp. 223\u2013234 (1976)"},{"key":"3_CR22","unstructured":"Bauer, F.L.: From specifications to machine code: Program construction through formal reasoning. In: Ohno, Y., Basili, V., Enomoto, H., Kobayashi, K., Yeh, R.T. (eds.) International Conference on Software Engineering, IEEE Computer Society, pp. 84\u201391 (1982)"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Bauer, F.L., W\u00f6ssner, H.: Algorithmic Language and Program Development. Texts and Monographs in Computer Science. Springer (1982). https:\/\/doi.org\/10.1007\/978-3-642-61807-9","DOI":"10.1007\/978-3-642-61807-9"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Bauer, F.L., et al.: The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L. Lecture Notes in Computer Science, vol. 183. Springer (1985). https:\/\/doi.org\/10.1007\/3-540-15187-7","DOI":"10.1007\/3-540-15187-7"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Bauer, F.L., et al.: The Munich Project CIP, Volume II: The Program Transformation System CIP-S, Lecture Notes in Computer Science, vol. 292. Springer-Verlag, Berlin (1987). https:\/\/doi.org\/10.1007\/3-540-18779-0","DOI":"10.1007\/3-540-18779-0"},{"key":"3_CR26","unstructured":"Bemer, R.: A politico-social history of ALGOL. In: Annual Review of Automatic Programming 5, pp. 151\u2013237. Pergamon Press, Oxford (1969)"},{"issue":"4","key":"3_CR27","first-page":"265","volume":"10","author":"M Benke","year":"2003","unstructured":"Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic J. Comput. 10(4), 265\u2013289 (2003)","journal-title":"Nordic J. Comput."},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/s001650050047","volume":"11","author":"R Bird","year":"1999","unstructured":"Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects Comput. 11(2), 200\u2013222 (1999). https:\/\/doi.org\/10.1007\/s001650050047","journal-title":"Formal Aspects Comput."},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Bird, R., Gibbons, J., Mehner, S., Voigtl\u00e4nder, J., Schrijvers, T.: Understanding idiomatic traversals backwards and forwards. In: Haskell Symposium. ACM (2013). https:\/\/doi.org\/10.1145\/25037782503781 (2013)","DOI":"10.1145\/25037782503781"},{"key":"3_CR30","unstructured":"Bird, R.S.: Some notational suggestions for transformational programming. Working Paper NIJ-3, IFIP WG2.1, also Technical Report RCS 144, Department of Computer Science, University of Reading (1981)"},{"key":"3_CR31","unstructured":"Bird, R.S.: An introduction to the theory of lists. Monograph PRG-56, Programming Research Group, University of Oxford (1986)"},{"key":"3_CR32","unstructured":"Bird, R.S.: A calculus of functions for program derivation. Monograph PRG-64, Programming Research Group, University of Oxford (1987)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Bird, R.S.: Lectures on constructive functional programming. Monograph PRG-69, Programming Research Group, University of Oxford (1988)","DOI":"10.1007\/978-3-642-74884-4_5"},{"issue":"3","key":"3_CR34","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1017\/S0956796801003914","volume":"11","author":"RS Bird","year":"2001","unstructured":"Bird, R.S.: Unfolding pointer algorithms. J. Funct. Program. 11(3), 347\u2013358 (2001). https:\/\/doi.org\/10.1017\/S0956796801003914","journal-title":"J. Funct. Program."},{"key":"3_CR35","unstructured":"Bird, R.S., de Moor, O.: Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Hoboken (1997)"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Blaine, L., Gilham, L., Liu, J., Smith, D.R., Westfold, S.J.: Planware: domain-specific synthesis of high-performance schedulers. In: Automated Software Engineering, IEEE Computer Society, p. 270 (1998). https:\/\/doi.org\/10.1109\/ASE.1998.732672","DOI":"10.1109\/ASE.1998.732672"},{"key":"3_CR37","unstructured":"Blikle, A.: Iterative systems: An algebraic approach. Bulletin de l\u2019Acad\u00e9mie Polonaise des Sciences, S\u00e9rie des sciences math\u00e9matiques, astronomiques et physiques XX(1) (1972)"},{"key":"3_CR38","unstructured":"Boom, H.: Further thoughts on Abstracto. Working Paper ELC-9, IFIP WG2.1 (1981)"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Botta, N., Jansson, P., Ionescu, C.: Contributions to a computational theory of policy advice and avoidability. J. Funct. Programm. 27, e23 (2017) . https:\/\/doi.org\/10.1017\/S0956796817000156","DOI":"10.1017\/S0956796817000156"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Botta, N., Jansson, P., Ionescu, C., Christiansen, D.R., Brady, E.: Sequential decision problems, dependent types and generic solutions. Logical Meth. Comput. Sci. 13(1) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(1:7)2017","DOI":"10.23638\/LMCS-13(1:7)2017"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Boyle, J., Harmer, T.J., Winter, V.L.: The TAMPR program transformation system: simplifying the development of numerical software. In: Arge, E., Bruaset, A.M., Langtangen, H.P. (eds,) Modern Software Tools for Scientific Computing, Birkh\u00e4user, pp. 353\u2013372 (1996) . https:\/\/doi.org\/10.1007\/978-1-4612-1986-6_17","DOI":"10.1007\/978-1-4612-1986-6_17"},{"key":"3_CR42","unstructured":"Boyle, J.M.: An introduction to Transformation-Assisted Multiple Program Realization (TAMPR) system. In: Bunch, J.R. (ed.) Cooperative Development of Mathematical Software, Department of Mathematics, University of California, San Diego (1976)"},{"key":"3_CR43","unstructured":"Boyle, J.M., Dritz, K.W.: An automated programming system to facilitate the development of quality mathematical software. In: Rosenfeld, J. (ed.) IFIP Congress, North-Holland, pp. 542\u2013546 (1974)"},{"issue":"5","key":"3_CR44","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: International Conference on Functional Programming, pp. 133\u2013144 (2013)","DOI":"10.1145\/2500365.2500581"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Broy, M.: Program construction by transformations: a family tree of sorting programs. In: Biermann, A., Guiho, G. (eds.) Computer Program Synthesis Methodologies, NATO Advanced Study Institutes Series, vol. 95. Springer (1983). https:\/\/doi.org\/10.1007\/978-94-009-7019-9_1","DOI":"10.1007\/978-94-009-7019-9_1"},{"key":"3_CR47","unstructured":"Broy, M., Pepper, P.: On the coherence of programming language and programming methodology. In: Bormann, (ed.) IFIP Working Conference on Programming Languages and System Design, North-Holland, pp. 41\u201353 (1983)"},{"key":"3_CR48","unstructured":"Burge, W.H.: Recursive Programming Techniques. Addison-Wesley, Boston (1975)"},{"issue":"1","key":"3_CR49","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977)","journal-title":"J. ACM"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Chakravarty, M.M.T., Keller, G., Jones, S.L.P., Marlow, S.: Associated types with class. In: Palsberg, J., Abadi, M. (eds.) Principles of Programming Languages. ACM, pp. 1\u201313 (2005). https:\/\/doi.org\/10.1145\/1040305.1040306","DOI":"10.1145\/1040305.1040306"},{"key":"3_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45\u201359. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722010_4"},{"key":"3_CR52","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1093\/comjnl\/9.1.45","volume":"9","author":"D Cooper","year":"1966","unstructured":"Cooper, D.: The equivalence of certain computations. Comput. J. 9, 45\u201352 (1966)","journal-title":"Comput. J."},{"key":"3_CR53","unstructured":"Dagand, P.E., et al.: A cosmology of datatypes: Reusability and dependent types. Ph.D. thesis, University of Strathclyde (2013)"},{"key":"3_CR54","doi-asserted-by":"crossref","unstructured":"Dang, H., M\u00f6ller, B.: Concurrency and local reasoning under reverse exchange. Sci. Comput. Programm. 85, Part B, 204\u2013223 (2013)","DOI":"10.1016\/j.scico.2013.07.006"},{"issue":"3","key":"3_CR55","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/j.jlamp.2014.12.002","volume":"84","author":"H Dang","year":"2015","unstructured":"Dang, H., M\u00f6ller, B.: Extended transitive separation logic. J. Logical Algebraic Meth. Programm. 84(3), 303\u2013325 (2015). https:\/\/doi.org\/10.1016\/j.jlamp.2014.12.002","journal-title":"J. Logical Algebraic Meth. Programm."},{"issue":"6","key":"3_CR56","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.jlap.2011.04.003","volume":"80","author":"H Dang","year":"2011","unstructured":"Dang, H., H\u00f6fner, P., M\u00f6ller, B.: Algebraic separation logic. J. Logic Algebraic Programm. 80(6), 221\u2013247 (2011). https:\/\/doi.org\/10.1016\/j.jlap.2011.04.003","journal-title":"J. Logic Algebraic Programm."},{"key":"3_CR57","unstructured":"Danielsson, N.A.: Functional program correctness through types. Ph.D. thesis, Chalmers University of Technology and Gothenburg University (2007)"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Total parser combinators. In: International Conference on Functional Programming, pp. 285\u2013296 (2010)","DOI":"10.1145\/1863543.1863585"},{"key":"3_CR59","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Correct-by-construction pretty-printing. In: Workshop on Dependently-Typed Programming, pp. 1\u201312 (2013)","DOI":"10.1145\/2502409.2502410"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Desharnais, J., M\u00f6ller, B.: Non-associative Kleene algebra and temporal logics. In: H\u00f6fner, P., Pous, D., Struth, G. (eds.) Relational and Algebraic Methods in Computer Science. Lecture Notes in Computer Science, vol. 10226, pp. 93\u2013108 (2017). https:\/\/doi.org\/10.1007\/978-3-319-57418-9_6","DOI":"10.1007\/978-3-319-57418-9_6"},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Termination in modal Kleene algebra. In: Mayr, E.W., Mitchell, J.C., L\u00e9vy, J.J. (eds.) Exploring New Frontiers of Theoretical Informatics, pp. 647\u2013660, Kluwer (2004)","DOI":"10.1007\/1-4020-8141-3_49"},{"issue":"4","key":"3_CR62","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798\u2013833 (2006)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"3_CR63","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.jlap.2005.04.006","volume":"66","author":"J Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Tchier, F.: Kleene under a modal demonic star. J. Logic Algebraic Programm. 66(2), 127\u2013160 (2006). https:\/\/doi.org\/10.1016\/j.jlap.2005.04.006","journal-title":"J. Logic Algebraic Programm."},{"key":"3_CR64","unstructured":"Dewar, R.: Letter to members of IFIP WG2.1 (1977). http:\/\/ershov-arc.iis.nsk.su\/archive\/eaindex.asp?did=29067"},{"key":"3_CR65","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Hoboken (1976)"},{"key":"3_CR66","doi-asserted-by":"publisher","unstructured":"Doornbos, H., Backhouse, R.C.: Algebra of program termination. In: Backhouse, R.C., Crole, R.L., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 2297, pp. 203\u2013236. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-47797-7_6","DOI":"10.1007\/3-540-47797-7_6"},{"key":"3_CR67","unstructured":"Feather, M.S.: A system for developing programs by transformation. Ph.D thesis, University of Edinburgh, UK (1979). http:\/\/hdl.handle.net\/1842\/7296"},{"issue":"1","key":"3_CR68","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/357153.357154","volume":"4","author":"MS Feather","year":"1982","unstructured":"Feather, M.S.: A system for assisting program transformation. ACM Trans. Programm. Lang. 4(1), 1\u201320 (1982). https:\/\/doi.org\/10.1145\/357153.357154","journal-title":"ACM Trans. Programm. Lang."},{"key":"3_CR69","unstructured":"Feather, M.S.: A survey and classification of some program transformation approaches and techniques. In: Meertens, L. (ed.) Program Specification and Transformation, North-Holland, pp. 165\u2013195 (1987)"},{"key":"3_CR70","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, American Mathematical Society, Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"3_CR71","unstructured":"Fokkinga, M.: Tupling and mutumorphisms. The Squiggolist 1(4), 81\u201382 (1990)"},{"key":"3_CR72","doi-asserted-by":"crossref","unstructured":"Brooks, J.F.: The Mythical Man-Month. Addison-Wesley, Boston (1975)","DOI":"10.1145\/800027.808439"},{"key":"3_CR73","unstructured":"Geurts, L., Meertens, L.: Remarks on Abstracto. Algol. Bull. 42, 56\u201363 (1978)"},{"key":"3_CR74","unstructured":"Geurts, L., Meertens, L., Pemberton, S.: The ABC Programmer\u2019s Handbook. Prentice-Hall, Hoboken, iSBN 0-13-000027-2 (1990)"},{"key":"3_CR75","doi-asserted-by":"publisher","unstructured":"Gibbons, J.: Free delivery (functional pearl). In: Haskell Symposium, pp. 45\u201350 (2016). https:\/\/doi.org\/10.1145\/2976002.2976005","DOI":"10.1145\/2976002.2976005"},{"key":"3_CR76","doi-asserted-by":"crossref","unstructured":"Gibbons, J.: The school of Squiggol: A history of the Bird-Meertens formalism. In: Astarte, T. (ed.) Workshop on the History of Formal Methods. Springer-Verlag, Lecture Notes in Computer Science (2020). (to appear)","DOI":"10.1007\/978-3-030-54997-8_2"},{"key":"3_CR77","doi-asserted-by":"publisher","unstructured":"Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: International Conference on Functional Programming, pp. 2\u201314 (2011). https:\/\/doi.org\/10.1145\/2034773.2034777","DOI":"10.1145\/2034773.2034777"},{"key":"3_CR78","doi-asserted-by":"publisher","unstructured":"Gibbons, J., dos Santos Oliveira, B.C.: The essence of the iterator pattern. J. Funct. Programm. 19(3,4), 377\u2013402 (2009). https:\/\/doi.org\/10.1017\/S0956796809007291","DOI":"10.1017\/S0956796809007291"},{"key":"3_CR79","doi-asserted-by":"publisher","unstructured":"Gibbons, J., Henglein, F., Hinze, R., Wu, N.: Relational algebra by way of adjunctions. Proc. ACM Programm. Lang. 2(ICFP), 86:1\u201386:28 (2018). https:\/\/doi.org\/10.1145\/3236781","DOI":"10.1145\/3236781"},{"key":"3_CR80","unstructured":"Gomes, V.B.F., Guttmann, W., H\u00f6fner, P., Struth, G., Weber, T.: Kleene algebras with domain. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/KAD.html"},{"key":"3_CR81","unstructured":"Green, C., et al.: Research on knowledge-based programming and algorithm design. Technical report Kes.U.81.2, Kestrel Institute (1981, revised 1982) (1981)"},{"issue":"3","key":"3_CR82","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1016\/j.jlamp.2014.08.001","volume":"84","author":"W Guttmann","year":"2015","unstructured":"Guttmann, W.: Infinite executions of lazy and strict computations. J. Logical Algebraic Meth. Programm. 84(3), 326\u2013340 (2015). https:\/\/doi.org\/10.1016\/j.jlamp.2014.08.001","journal-title":"J. Logical Algebraic Meth. Programm."},{"key":"3_CR83","unstructured":"Guttmann, W.: Stone algebras. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Stone_Algebras.html"},{"key":"3_CR84","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.tcs.2018.04.012","volume":"744","author":"W Guttmann","year":"2018","unstructured":"Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theoret. Comput. Sci. 744, 37\u201355 (2018)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"3_CR85","doi-asserted-by":"publisher","first-page":"173","DOI":"10.3217\/jucs-009-02-0173","volume":"9","author":"W Guttmann","year":"2003","unstructured":"Guttmann, W., Partsch, H., Schulte, W., Vullinghs, T.: Tool support for the interactive derivation of formally correct functional programs. J. Univ. Comput. Sci. 9(2), 173 (2003). https:\/\/doi.org\/10.3217\/jucs-009-02-0173","journal-title":"J. Univ. Comput. Sci."},{"key":"3_CR86","unstructured":"Hagino, T.: A categorical programming language. Ph.D thesis, University of Edinburgh, UK (1987)"},{"issue":"2","key":"3_CR87","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/69610.357988","volume":"27","author":"ECR Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming, part I. Commun. ACM 27(2), 134\u2013143 (1984). https:\/\/doi.org\/10.1145\/69610.357988","journal-title":"Commun. ACM"},{"issue":"2","key":"3_CR88","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/69610.357990","volume":"27","author":"ECR Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming, part II. Commun. ACM 27(2), 144\u2013151 (1984). https:\/\/doi.org\/10.1145\/69610.357990","journal-title":"Commun. ACM"},{"key":"3_CR89","doi-asserted-by":"publisher","unstructured":"Hehner, E.C.R.: A Practical Theory of Programming. Springer (1993). https:\/\/doi.org\/10.1007\/978-1-4419-8596-5_7","DOI":"10.1007\/978-1-4419-8596-5_7"},{"issue":"3","key":"3_CR90","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/S0167-6423(98)00027-6","volume":"34","author":"ECR Hehner","year":"1999","unstructured":"Hehner, E.C.R.: Specifications, programs, and total correctness. Sci. Comput. Program. 34(3), 191\u2013205 (1999). https:\/\/doi.org\/10.1016\/S0167-6423(98)00027-6","journal-title":"Sci. Comput. Program."},{"issue":"2\u20133","key":"3_CR91","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0167-6423(02)00025-4","volume":"43","author":"R Hinze","year":"2002","unstructured":"Hinze, R.: Polytypic values possess polykinded types. Sci. Comput. Program. 43(2\u20133), 129\u2013159 (2002)","journal-title":"Sci. Comput. Program."},{"issue":"11","key":"3_CR92","doi-asserted-by":"publisher","first-page":"2108","DOI":"10.1016\/j.scico.2012.07.011","volume":"78","author":"R Hinze","year":"2013","unstructured":"Hinze, R.: Adjoint folds and unfolds\u2013an extended study. Sci. Comput. Program. 78(11), 2108\u20132159 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.07.011","journal-title":"Sci. Comput. Program."},{"key":"3_CR93","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1017\/S0956796815000258","volume":"26","author":"R Hinze","year":"2016","unstructured":"Hinze, R., Wu, N.: Unifying structured recursion schemes: an extended study. J. Funct. Program. 26, 47 (2016)","journal-title":"J. Funct. Program."},{"issue":"1\u20132","key":"3_CR94","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.scico.2003.07.001","volume":"51","author":"R Hinze","year":"2004","unstructured":"Hinze, R., Jeuring, J., L\u00f6h, A.: Type-indexed data types. Sci. Comput. Program. 51(1\u20132), 117\u2013151 (2004)","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"3_CR95","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"3_CR96","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Programs are predicates. Philosophical Transactions of the Royal Society of London (A 312), 475\u2013489 (1984)","DOI":"10.1098\/rsta.1984.0071"},{"issue":"8","key":"3_CR97","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987). https:\/\/doi.org\/10.1145\/27651.27653","journal-title":"Commun. ACM"},{"issue":"6","key":"3_CR98","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.jlap.2011.04.005","volume":"80","author":"T Hoare","year":"2011","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Logic Algebraic Programm. 80(6), 266\u2013296 (2011). https:\/\/doi.org\/10.1016\/j.jlap.2011.04.005","journal-title":"J. Logic Algebraic Programm."},{"key":"3_CR99","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.jlap.2007.10.004","volume":"76","author":"P H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: Algebraic neighbourhood logic. J. Logic Algebraic Programm. 76, 35\u201359 (2008)","journal-title":"J. Logic Algebraic Programm."},{"key":"3_CR100","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.jlap.2008.08.005","volume":"78","author":"P H\u00f6fner","year":"2009","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: An algebra of hybrid systems. J. Logic Algebraic Programm. 78, 74\u201397 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.005","journal-title":"J. Logic Algebraic Programm."},{"issue":"28","key":"3_CR101","doi-asserted-by":"publisher","first-page":"3303","DOI":"10.1016\/j.tcs.2011.03.018","volume":"412","author":"P H\u00f6fner","year":"2011","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: Fixing Zeno gaps. Theoret. Comput. Sci. 412(28), 3303\u20133322 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.03.018","journal-title":"Theoret. Comput. Sci."},{"issue":"4\u20136","key":"3_CR102","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00165-012-0245-4","volume":"24","author":"P H\u00f6fner","year":"2012","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: Dijkstra, Floyd and Warshall meet Kleene. Formal Aspects Comput. 24(4\u20136), 459\u2013476 (2012). https:\/\/doi.org\/10.1007\/s00165-012-0245-4","journal-title":"Formal Aspects Comput."},{"key":"3_CR103","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279\u2013294. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_19"},{"key":"3_CR104","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-78913-0_16","volume-title":"Relations and Kleene Algebra in Computer Science","author":"P H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: Non-termination in idempotent semirings. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2008. LNCS, vol. 4988, pp. 206\u2013220. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78913-0_16"},{"key":"3_CR105","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Reasoning","author":"P H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 50\u201366. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_5"},{"issue":"1\u20132","key":"3_CR106","first-page":"245","volume":"5","author":"P H\u00f6fner","year":"2011","unstructured":"H\u00f6fner, P., Kh\u00e9dri, R., M\u00f6ller, B.: Supplementing product families with behaviour. Softw. Inform. 5(1\u20132), 245\u2013266 (2011)","journal-title":"Softw. Inform."},{"issue":"4","key":"3_CR107","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1017\/S0956796898003050","volume":"8","author":"G Hutton","year":"1998","unstructured":"Hutton, G., Meijer, E.: Monadic parsing in Haskell. J. Funct. Program. 8(4), 437\u2013444 (1998). https:\/\/doi.org\/10.1017\/S0956796898003050","journal-title":"J. Funct. Program."},{"issue":"1","key":"3_CR108","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1017\/S0960129514000139","volume":"26","author":"C Ionescu","year":"2016","unstructured":"Ionescu, C.: Vulnerability modelling with functional programming and dependent types. Math. Struct. Comput. Sci. 26(1), 114\u2013128 (2016). https:\/\/doi.org\/10.1017\/S0960129514000139","journal-title":"Math. Struct. Comput. Sci."},{"key":"3_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-41582-1_9","volume-title":"Implementation and Application of Functional Languages","author":"C Ionescu","year":"2013","unstructured":"Ionescu, C., Jansson, P.: Dependently-typed programming in scientific computing. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 140\u2013156. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41582-1_9"},{"key":"3_CR110","doi-asserted-by":"publisher","unstructured":"Ionescu, C., Jansson, P.: Testing versus proving in climate impact research. In: TYPES 2011, Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 19, pp. 41\u201354 (2013). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2011.41","DOI":"10.4230\/LIPIcs.TYPES.2011.41"},{"key":"3_CR111","doi-asserted-by":"crossref","unstructured":"Jansson, P., Jeuring, J.: PolyP \u2013 a polytypic programming language extension. In: Principles of Programming Languages, pp. 470\u2013482 (1997)","DOI":"10.1145\/263699.263763"},{"key":"3_CR112","unstructured":"Jeuring, J., Meertens, L.: Geniaal programmeren-generic programming at Utrecht-. In: et al. HB (ed.) Fascination for computation, 25 jaar opleiding informatica, Department of Information and Computing Sciences, Utrecht University, pp. 75\u201388 (2009)"},{"key":"3_CR113","doi-asserted-by":"publisher","unstructured":"Johnson, W.L., Feather, M.S., Harris, D.R.: The KBSA requirements\/specifications facet: ARIES. In: Knowledge-Based Software Engineering, IEEE Computer Society, pp. 48\u201356 (1991). https:\/\/doi.org\/10.1109\/KBSE.1991.638020","DOI":"10.1109\/KBSE.1991.638020"},{"key":"3_CR114","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1093\/jigpal\/6.2.157","volume":"6","author":"B von Karger","year":"1998","unstructured":"von Karger, B., Berghammer, R.: A relational model for temporal logic. Logic J. IGPL 6, 157\u2013173 (1998)","journal-title":"Logic J. IGPL"},{"key":"3_CR115","unstructured":"Ko, H.S.: Analysis and synthesis of inductive families. DPhil thesis, Oxford University, UK (2014)"},{"issue":"3","key":"3_CR116","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"3_CR117","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60\u201376 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"3_CR118","doi-asserted-by":"crossref","unstructured":"L\u00e4mmel, R., Jones, S.P.: Scrap your boilerplate: a practical design pattern for generic programming. In: Types in Language Design and Implementation, pp. 26\u201337 (2003)","DOI":"10.1145\/604174.604179"},{"key":"3_CR119","doi-asserted-by":"crossref","unstructured":"L\u00f6h, A., Clarke, D., Jeuring, J.: Dependency-style generic Haskell. In: Shivers, O. (ed.) International Conference on Functional Programming. ACM Press, pp. 141\u2013152 (2003)","DOI":"10.1145\/944705.944719"},{"issue":"2","key":"3_CR120","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0167-6423(82)90010-7","volume":"2","author":"P London","year":"1982","unstructured":"London, P., Feather, M.: Implementing specification freedoms. Sci. Comput. Program. 2(2), 91\u2013131 (1982)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"3_CR121","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s00165-014-0316-9","volume":"27","author":"H Macedo","year":"2015","unstructured":"Macedo, H., Oliveira, J.N.: A linear algebra approach to OLAP. Formal Aspects Comput. 27(2), 283\u2013307 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0316-9","journal-title":"Formal Aspects Comput."},{"key":"3_CR122","doi-asserted-by":"crossref","unstructured":"Magalh\u00e3es, J.P., Dijkstra, A., Jeuring, J., L\u00f6h, A.: A generic deriving mechanism for Haskell. In: Haskell Symposium, pp. 37\u201348 (2010)","DOI":"10.1145\/1863523.1863529"},{"key":"3_CR123","unstructured":"Magalh\u00e3es, J.P.R.: Less is more: generic programming theory and practice. PhD thesis, Utrecht University, Netherlands (2012)"},{"key":"3_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs","author":"L Magnusson","year":"1994","unstructured":"Magnusson, L., Nordstr\u00f6m, B.: The ALF proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 213\u2013237. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58085-9_78"},{"key":"3_CR125","unstructured":"Malcolm, G.: Algebraic data types and program transformation. PhD thesis, University of Groningen (1990)"},{"key":"3_CR126","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","volume":"14","author":"G Malcolm","year":"1990","unstructured":"Malcolm, G.: Data structures and program transformation. Sci. Comput. Program. 14, 255\u2013279 (1990)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"3_CR127","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1109\/TSE.1979.234198","volume":"5","author":"Z Manna","year":"1979","unstructured":"Manna, Z., Waldinger, R.J.: Synthesis: dreams $$\\rightarrow $$ programs. IEEE Trans. Software Eng. 5(4), 294\u2013328 (1979). https:\/\/doi.org\/10.1109\/TSE.1979.234198","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"3_CR128","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980). https:\/\/doi.org\/10.1145\/357084.357090","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR129","unstructured":"Manna, Z., Waldinger, R.J.: The Deductive Foundations of Computer Programming. Addison-Wesley, Boston (1993)"},{"key":"3_CR130","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Studies in Logic and the Foundations of Mathematics, vol. 104, Elsevier, pp. 153\u2013175 (1982)","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"3_CR131","doi-asserted-by":"publisher","unstructured":"McBride, C.: How to keep your neighbours in order. In: International Conference on Functional Programming, Association for Computing Machinery, New York, NY, USA, ICFP 2014, pp. 297\u2013309 (2014). https:\/\/doi.org\/10.1145\/2628136.2628163","DOI":"10.1145\/2628136.2628163"},{"issue":"1","key":"3_CR132","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"issue":"1","key":"3_CR133","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008). https:\/\/doi.org\/10.1017\/S0956796807006326","journal-title":"J. Funct. Program."},{"key":"3_CR134","unstructured":"McKinna, J., Wright, J.: A type-correct, stack-safe, provably correct, expression compiler in Epigram, unpublished draft (2006)"},{"key":"3_CR135","doi-asserted-by":"crossref","unstructured":"Meertens, L.: Abstracto 84: The next generation. In: Proceedings of the 1979 Annual Conference. ACM, pp. 33\u201339 (1979)","DOI":"10.1145\/800177.810022"},{"key":"3_CR136","unstructured":"Meertens, L.: Algorithmics: Towards programming as a mathematical activity. In: de Bakker, J.W., Hazewinkel, M., Lenstra, J.K. (eds.) Proceedings of the CWI Symposium on Mathematics and Computer Science, North-Holland, pp. 289\u2013334 (1986). https:\/\/ir.cwi.nl\/pub\/20634"},{"key":"3_CR137","unstructured":"Meertens, L.: An Abstracto reader prepared for IFIP WG 2.1. Technical report CS-N8702, CWI, Amsterdam (1987)"},{"key":"3_CR138","unstructured":"Meertens, L.: Squiggol versus Squigol, private email to JG (2019)"},{"issue":"5","key":"3_CR139","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/BF01211391","volume":"4","author":"LGLT Meertens","year":"1992","unstructured":"Meertens, L.G.L.T.: Paramorphisms. Formal Aspects Comput. 4(5), 413\u2013424 (1992)","journal-title":"Formal Aspects Comput."},{"key":"3_CR140","doi-asserted-by":"publisher","unstructured":"Meijer, E., Fokkinga, M.M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes, J. (ed.) Functional Programming Languages and Computer Architecture. Lecture Notes in Computer Science, vol. 523. Springer, pp. 124\u2013144 (1991). https:\/\/doi.org\/10.1007\/3540543961_7","DOI":"10.1007\/3540543961_7"},{"issue":"1","key":"3_CR141","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"3_CR142","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, B.: Calculating with pointer structures. In: IFIP TC2\/WG 2.1 Working Conference on Algorithmic Languages and Calculi, pp. 24\u201348. Chapman & Hall (1997)","DOI":"10.1007\/978-0-387-35264-0_2"},{"key":"3_CR143","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.scico.2006.01.010","volume":"65","author":"B M\u00f6ller","year":"2007","unstructured":"M\u00f6ller, B.: Kleene getting lazy. Sci. Comput. Program. 65, 195\u2013214 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"3_CR144","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1093\/comjnl\/bxs140","volume":"56","author":"B M\u00f6ller","year":"2013","unstructured":"M\u00f6ller, B.: Modal knowledge and game semirings. Comput. J. 56(1), 53\u201369 (2013). https:\/\/doi.org\/10.1093\/comjnl\/bxs140","journal-title":"Comput. J."},{"key":"3_CR145","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/j.jlamp.2019.02.003","volume":"104","author":"B M\u00f6ller","year":"2019","unstructured":"M\u00f6ller, B.: Geographic wayfinders and space-time algebra. J. Logical Algebraic Meth. Programm. 104, 274\u2013302 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2019.02.003","journal-title":"J. Logical Algebraic Meth. Programm."},{"issue":"3","key":"3_CR146","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1016\/j.jlamp.2015.01.001","volume":"84","author":"B M\u00f6ller","year":"2015","unstructured":"M\u00f6ller, B., Roocks, P.: An algebra of database preferences. J. Logical Algebraic Meth. Programm. 84(3), 456\u2013481 (2015). https:\/\/doi.org\/10.1016\/j.jlamp.2015.01.001","journal-title":"J. Logical Algebraic Meth. Programm."},{"key":"3_CR147","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-540-27815-3_30","volume-title":"Algebraic Methodology and Software Technology","author":"B M\u00f6ller","year":"2004","unstructured":"M\u00f6ller, B., Struth, G.: Modal Kleene algebra and partial correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 379\u2013393. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27815-3_30"},{"key":"3_CR148","doi-asserted-by":"publisher","unstructured":"M\u00f6ller, B., Struth, G.: wp Is wlp. In: MacCaull, W., Winter, W., D\u00fcntsch, I. (eds.) Relational Methods in Computer Science. Lecture Notes in Computer Science, vol. 3929, pp. 200\u2013211. Springer (2005). https:\/\/doi.org\/10.1007\/11734673_16","DOI":"10.1007\/11734673_16"},{"key":"3_CR149","unstructured":"M\u00f6ller, B., Partsch, H., Pepper, P.: Programming with transformations: an overview of the Munich CIP project (1983)"},{"key":"3_CR150","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/11784180_21","volume-title":"Algebraic Methodology and Software Technology","author":"B M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., H\u00f6fner, P., Struth, G.: Quantales and temporal logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 263\u2013277. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11784180_21"},{"issue":"3","key":"3_CR151","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C Morgan","year":"1988","unstructured":"Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10(3), 403\u2013419 (1988). https:\/\/doi.org\/10.1145\/44501.44503","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR152","volume-title":"Programming from Specifications","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall, Hoboken (1990)"},{"key":"3_CR153","doi-asserted-by":"publisher","unstructured":"Morgan, C.: An old new notation for elementary probability theory. Sci. Comput. Program. 85, 115\u2013136 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.09.003. special Issue on Mathematics of Program Construction 2012","DOI":"10.1016\/j.scico.2013.09.003"},{"issue":"3","key":"3_CR154","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"JM Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"3_CR155","unstructured":"Morris, P.W.: Constructing universes for generic programming. PhD thesis, University of Nottingham, UK (2007)"},{"issue":"5","key":"3_CR156","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1017\/S0956796809007345","volume":"19","author":"SC Mu","year":"2009","unstructured":"Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545\u2013579 (2009)","journal-title":"J. Funct. Program."},{"key":"3_CR157","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: International Conference on Functional Programming, pp. 62\u201373 (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"3_CR158","unstructured":"Naur, P.: The IFIP working group on ALGOL. ALGOL Bull. (Issue 15), 52 (1962)"},{"key":"3_CR159","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)"},{"key":"3_CR160","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.: Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375, 271\u2013307 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR161","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"3_CR162","doi-asserted-by":"publisher","unstructured":"Paige, R.: Transformational programming \u2013 Applications to algorithms and systems. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Principles of Programming Languages. ACM, pp. 73\u201387 (1983). https:\/\/doi.org\/10.1145\/567067.567076","DOI":"10.1145\/567067.567076"},{"key":"3_CR163","doi-asserted-by":"crossref","unstructured":"Pardo, A.: Generic accumulations. In: Gibbons, J., Jeuring, J. (eds.) Generic Programming: IFIP TC2\/WG2.1 Working Conference on Generic Programming. Kluwer Academic Publishers, International Federation for Information Processing, vol. 115, pp. 49\u201378 (2002)","DOI":"10.1007\/978-0-387-35672-3_3"},{"key":"3_CR164","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/3-540-10007-5_47","volume-title":"Abstract Software Specifications","author":"D Park","year":"1980","unstructured":"Park, D.: On the semantics of fair parallelism. In: Bj\u00f8orner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504\u2013526. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10007-5_47"},{"issue":"1","key":"3_CR165","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(83)90002-3","volume":"3","author":"H Partsch","year":"1983","unstructured":"Partsch, H.: An exercise in the transformational derivation of an efficient program by joing development of control and data structure. Sci. Comput. Program. 3(1), 1\u201335 (1983). https:\/\/doi.org\/10.1016\/0167-6423(83)90002-3","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"3_CR166","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0167-6423(84)90010-8","volume":"4","author":"H Partsch","year":"1984","unstructured":"Partsch, H.: Structuring transformational developments: a case study based on Earley\u2019s recognizer. Sci. Comput. Program. 4(1), 17\u201344 (1984). https:\/\/doi.org\/10.1016\/0167-6423(84)90010-8","journal-title":"Sci. Comput. Program."},{"key":"3_CR167","doi-asserted-by":"publisher","unstructured":"Partsch, H.: Transformational derivation of parsing algorithms executable on parallel architectures. In: Ammann. U. (ed.) Programmiersprachen und Programmentwicklung, Informatik-Fachberichte, vol. 77, pp. 41\u201357. Springer (1984). https:\/\/doi.org\/10.1007\/978-3-642-69393-9_3","DOI":"10.1007\/978-3-642-69393-9_3"},{"issue":"2","key":"3_CR168","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0167-6423(86)90008-0","volume":"7","author":"H Partsch","year":"1986","unstructured":"Partsch, H.: Transformational program development in a particular program domain. Sci. Comput. Program. 7(2), 99\u2013241 (1986). https:\/\/doi.org\/10.1016\/0167-6423(86)90008-0","journal-title":"Sci. Comput. Program."},{"key":"3_CR169","doi-asserted-by":"publisher","unstructured":"Partsch, H.: Specification and Transformation of Programs \u2013 A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer (1990). https:\/\/doi.org\/10.1007\/978-3-642-61512-2","DOI":"10.1007\/978-3-642-61512-2"},{"issue":"3","key":"3_CR170","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/356914.356917","volume":"15","author":"H Partsch","year":"1983","unstructured":"Partsch, H., Steinbr\u00fcggen, R.: Program transformation systems. ACM Comput. Surv. 15(3), 199\u2013236 (1983)","journal-title":"ACM Comput. Surv."},{"key":"3_CR171","first-page":"317","volume":"9","author":"CS Peirce","year":"1870","unstructured":"Peirce, C.S.: Description of a notation for the logic of relatives, resulting from an amplification of the conceptions of Boole\u2019s calculus of logic. Memoirs Am. Acad. Arts Sci. 9, 317\u2013378 (1870)","journal-title":"Memoirs Am. Acad. Arts Sci."},{"issue":"2\u20133","key":"3_CR172","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/S0167-6423(96)00023-8","volume":"28","author":"P Pepper","year":"1997","unstructured":"Pepper, P., Smith, D.R.: A high-level derivation of global search algorithms (with constraint propagation). Sci. Comput. Program. 28(2\u20133), 247\u2013271 (1997). https:\/\/doi.org\/10.1016\/S0167-6423(96)00023-8","journal-title":"Sci. Comput. Program."},{"key":"3_CR173","unstructured":"Jones, S.P., et al.: Haskell 98, Language and Libraries. The Revised Report. Cambridge University Press, a special issue of the Journal of Functional Programming (2003)"},{"key":"3_CR174","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-60074-1_9","volume-title":"Grand Timely Topics in Software Engineering","author":"R Pontes","year":"2017","unstructured":"Pontes, R., Matos, M., Oliveira, J.N., Pereira, J.O.: Implementing a linear algebra approach to data processing. In: Cunha, J., Fernandes, J.P., L\u00e4mmel, R., Saraiva, J., Zaytsev, V. (eds.) GTTSE 2015. LNCS, vol. 10223, pp. 215\u2013222. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-60074-1_9"},{"key":"3_CR175","unstructured":"Pretnar, M.: The logic and handling of algebraic effects. PhD thesis, School of Informatics, University of Edinburgh (2010)"},{"key":"3_CR176","unstructured":"Python Software Foundation: Python website (1997). https:\/\/www.python.org\/"},{"key":"3_CR177","doi-asserted-by":"crossref","unstructured":"Yakushev, A.R., Jeuring, J., Jansson, P., Gerdes, A., Kiselyov, O., Oliveira, B.C.D.S.: Comparing libraries for generic programming in Haskell. In: Haskell Symposium, pp. 111\u2013122 (2008)","DOI":"10.1145\/1411286.1411301"},{"key":"3_CR178","doi-asserted-by":"crossref","unstructured":"Yakushev, A.R., Holdermans, S., L\u00f6h, A., Jeuring, J.: Generic programming with fixed points for mutually recursive datatypes. In: Hutton, G., Tolmach, A.P. (eds.) International Conference on Functional Programming, pp. 233\u2013244 (2009)","DOI":"10.1145\/1596550.1596585"},{"key":"3_CR179","unstructured":"Ruehr, F.: Dr Seuss on parser monads (2001). https:\/\/willamette.edu\/~fruehr\/haskell\/seuss.html"},{"key":"3_CR180","unstructured":"Schr\u00f6der, E.: Vorlesungen \u00fcber die Algebra der Logik, vol 3. Taubner (1895)"},{"key":"3_CR181","unstructured":"Schuman, S.A. (ed.): New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d\u2019Informatique et d\u2019Automatique (1975)"},{"key":"3_CR182","unstructured":"Schuman, S.A. (ed.): New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d\u2019Informatique et d\u2019Automatique (1976)"},{"issue":"1\u20132","key":"3_CR183","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0020-0190(03)00387-9","volume":"88","author":"M Sintzoff","year":"2003","unstructured":"Sintzoff, M.: On the design of correct and optimal dynamical systems and games. Inf. Process. Lett. 88(1\u20132), 59\u201365 (2003). https:\/\/doi.org\/10.1016\/S0020-0190(03)00387-9","journal-title":"Inf. Process. Lett."},{"key":"3_CR184","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-70594-9_18","volume-title":"Mathematics of Program Construction","author":"M Sintzoff","year":"2008","unstructured":"Sintzoff, M.: Synthesis of optimal control policies for some infinite-state transition systems. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 336\u2013359. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_18"},{"issue":"9","key":"3_CR185","doi-asserted-by":"publisher","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"DR Smith","year":"1990","unstructured":"Smith, D.R.: KIDS: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024\u20131043 (1990). https:\/\/doi.org\/10.1109\/32.58788","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"3_CR186","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0167-6423(90)90056-J","volume":"14","author":"JM Spivey","year":"1990","unstructured":"Spivey, J.M.: A functional theory of exceptions. Sci. Comput. Program. 14(1), 25\u201342 (1990). https:\/\/doi.org\/10.1016\/0167-6423(90)90056-J","journal-title":"Sci. Comput. Program."},{"key":"3_CR187","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-57499-9_26","volume-title":"Formal Program Development","author":"SD Swierstra","year":"1993","unstructured":"Swierstra, S.D., de Moor, O.: Virtual data structures. In: M\u00f6ller, B., Partsch, H., Schuman, S. (eds.) Formal Program Development. LNCS, vol. 755, pp. 355\u2013371. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57499-9_26"},{"key":"3_CR188","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-61628-4_7","volume-title":"Advanced Functional Programming","author":"SD Swierstra","year":"1996","unstructured":"Swierstra, S.D., Duponcheel, L.: Deterministic, error-correcting combinator parsers. In: Launchbury, J., Meijer, E., Sheard, T. (eds.) AFP 1996. LNCS, vol. 1129, pp. 184\u2013207. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61628-4_7"},{"key":"3_CR189","unstructured":"Swierstra, W.: A functional specification of effects. PhD thesis, University of Nottingham (2008)"},{"key":"3_CR190","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-319-29604-3_3","volume-title":"Functional and Logic Programming","author":"W Swierstra","year":"2016","unstructured":"Swierstra, W., Alpuim, J.: From proposition to program. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 29\u201344. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_3"},{"key":"3_CR191","doi-asserted-by":"crossref","unstructured":"Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Haskell Workshop, pp. 25\u201336 (2007). http:\/\/doi.acm.org\/10.1145\/1291201.1291206","DOI":"10.1145\/1291201.1291206"},{"key":"3_CR192","doi-asserted-by":"crossref","unstructured":"Swierstra, W., Baanen, T.: A predicate transformer semantics for effects (functional pearl). Proc. ACM Programm. Lang. 3(ICFP), 1\u201326 (2019)","DOI":"10.1145\/3341707"},{"key":"3_CR193","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/11783596_25","volume-title":"Mathematics of Program Construction","author":"A Tafliovich","year":"2006","unstructured":"Tafliovich, A., Hehner, E.C.R.: Quantum predicative programming. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 433\u2013454. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11783596_25"},{"issue":"3","key":"3_CR194","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73\u201389 (1941). https:\/\/doi.org\/10.2307\/2268577","journal-title":"J. Symb. Log."},{"issue":"1","key":"3_CR195","first-page":"5","volume":"10","author":"T Uustalu","year":"1999","unstructured":"Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10(1), 5\u201326 (1999)","journal-title":"Informatica"},{"issue":"5","key":"3_CR196","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/j.entcs.2008.05.029","volume":"203","author":"T Uustalu","year":"2008","unstructured":"Uustalu, T., Vene, V.: Comonadic notions of computation. Electron. Notes Theoer. Comput. Sci. 203(5), 263\u2013284 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2008.05.029","journal-title":"Electron. Notes Theoer. Comput. Sci."},{"issue":"3","key":"3_CR197","first-page":"366","volume":"8","author":"T Uustalu","year":"2001","unstructured":"Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nordic J. Comput. 8(3), 366\u2013390 (2001)","journal-title":"Nordic J. Comput."},{"key":"3_CR198","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Comprehending monads. In: LISP and Functional Programming. ACM, pp. 61\u201378 (1990). https:\/\/doi.org\/10.1145\/91556.91592","DOI":"10.1145\/91556.91592"},{"key":"3_CR199","doi-asserted-by":"publisher","unstructured":"Wadler, P.: The essence of functional programming. In: Principles of Programming Languages. ACM, pp. 1\u201314 (1992). https:\/\/doi.org\/10.1145\/143165.143169","DOI":"10.1145\/143165.143169"},{"issue":"12","key":"3_CR200","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015)","journal-title":"Commun. ACM"},{"key":"3_CR201","unstructured":"Wile, D.: POPART: producer of parsers and related tools: System builder\u2019s manual. USC\/ISI Information Science Institute, University of Southern California, Technical report (1981)"},{"key":"3_CR202","unstructured":"Wile, D.: Program developments as formal objects. USC\/ISI Information Science Institute, University of Southern California, Technical report (1981)"},{"key":"3_CR203","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Principles of Programming Languages, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["IFIP Advances in Information and Communication Technology","Advancing Research in Information and Communication Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81701-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T22:02:42Z","timestamp":1754172162000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81701-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030817008","9783030817015"],"references-count":203,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81701-5_3","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"4 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}