Nothing Special   »   [go: up one dir, main page]

Skip to main content

Abstract

Algorithmics is the study and practice of taking a high-level description of a program’s purpose and, from it, producing an executable program of acceptable efficiency. Each step in that process is justified by rigorous, careful reasoning at the moment it is taken; and the repertoire of steps allowed by that rigour, at each stage, guides the development of the algorithm itself.

IFIP’s Working Group 2.1 [i] has always been concerned with Algorithmics: both the design of its notations and the laws that enable its calculations. ALGOL 60 had already shown that orthogonality, simplicity and rigour in a programming language improves the quality of its programs.

Our Group’s title “Algorithmic Languages and Calculi” describes our activities: the discovery of precise but more general rules of calculational reasoning for the many new styles of programming that have developed over the 60 years since IFIP’s founding. As our contribution to the birthday celebrations, we outline how we have tried to contribute during those decades to the rigorous and reliable design of computer programs of all kinds—to Algorithmics. (Roman-numbered references like [i] in this abstract refer to details given in Sect. 10.)

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 99.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 129.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Aarts, C., et al.: Fixed-point calculus. Inf. Process. Lett. 53(3), 131–136 (1995)

    Article  MathSciNet  Google Scholar 

  2. Agresti, W.M.: What are the new paradigms? In: Agresti, W.M. (ed.) New Paradigms for Software Development. IEEE Computer Society Press (1986)

    Google Scholar 

  3. Alpuim, J., Swierstra, W.: Embedding the refinement calculus in Coq. Sci. Comput. Program. 164, 37–48 (2018)

    Article  Google Scholar 

  4. Altenkirch, T., Mcbride, C.: Generic programming within dependently typed programming. In: Gibbons, J., Jeuring, J. (eds.) Generic Programming. ITIFIP, vol. 115, pp. 1–20. Springer, Boston, MA (2003). https://doi.org/10.1007/978-0-387-35672-3_1

    Chapter  MATH  Google Scholar 

  5. Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013). http://isa-afp.org/entries/Kleene_Algebra.html

  6. Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs (2014). http://isa-afp.org/entries/Relation_Algebra.html

  7. Augustsson, L.: Cayenne - a language with dependent types. In: International Conference on Functional Programming, ICFP 1998, pp. 239–250 (1998)

    Google Scholar 

  8. 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)

    Google Scholar 

  9. Back, R.J.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49–68 (1981). https://doi.org/10.1016/0022-0000(81)90005-2

    Article  MathSciNet  MATH  Google Scholar 

  10. 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

  11. Backhouse, R.: An exploration of the Bird-Meertens formalism. Technical report CS 8810, Department of Computer Science, Groningen University (1988)

    Google Scholar 

  12. Backhouse, R., Michaelis, D.: Fixed-point characterisation of winning strategies in impartial games. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. Lecture Notes in Computer Science, vol. 3051, pp. 34–47. Springer (2004)

    Google Scholar 

  13. Backhouse, R., Chisholm, P., Malcolm, G., Saaman, E.: Do-it-yourself type theory. Formal Aspects Comput. 1(1), 19–84 (1989)

    Article  Google Scholar 

  14. 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

  15. Backhouse, R.C., Carré, B.A.: Regular algebra applied to path-finding problems. IMA J. Appl. Math. 15(2), 161–186 (1975). https://doi.org/10.1093/imamat/15.2.161

    Article  MathSciNet  MATH  Google Scholar 

  16. Backhouse, R.C., Doornbos, H.: Datatype-generic termination proofs. Theor. Comput. Syst. 43(3–4), 362–393 (2008). https://doi.org/10.1007/s00224-007-9056-z

    Article  MathSciNet  MATH  Google Scholar 

  17. Backhouse, R.C., Chen, W., Ferreira, J.F.: The algorithmics of solitaire-like games. Sci. Comput. Program. 78(11), 2029–2046 (2013). https://doi.org/10.1016/j.scico.2012.07.007

    Article  MATH  Google Scholar 

  18. Backhouse, R.C., Doornbos, H., Glück, R., van der Woude, J.: Elements of algorithmic graph theory: an exercise in point-free reasoning, (working document) (2019)

    Google Scholar 

  19. 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–344 (1976)

    Google Scholar 

  20. Batory, D.S., Höfner, P., Kim, J.: Feature interactions, products, and composition. In: Denney, E., Schultz, U.P. (eds.) Generative Programming and Component Engineering. ACM, pp. 13–22 (2011). https://doi.org/10.1145/2047862.2047867

  21. 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–234 (1976)

    Google Scholar 

  22. 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–91 (1982)

    Google Scholar 

  23. Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Texts and Monographs in Computer Science. Springer (1982). https://doi.org/10.1007/978-3-642-61807-9

  24. 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

  25. 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

  26. Bemer, R.: A politico-social history of ALGOL. In: Annual Review of Automatic Programming 5, pp. 151–237. Pergamon Press, Oxford (1969)

    Google Scholar 

  27. Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic J. Comput. 10(4), 265–289 (2003)

    MathSciNet  MATH  Google Scholar 

  28. Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects Comput. 11(2), 200–222 (1999). https://doi.org/10.1007/s001650050047

    Article  MATH  Google Scholar 

  29. Bird, R., Gibbons, J., Mehner, S., Voigtländer, J., Schrijvers, T.: Understanding idiomatic traversals backwards and forwards. In: Haskell Symposium. ACM (2013). https://doi.org/10.1145/25037782503781 (2013)

  30. 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)

    Google Scholar 

  31. Bird, R.S.: An introduction to the theory of lists. Monograph PRG-56, Programming Research Group, University of Oxford (1986)

    Google Scholar 

  32. Bird, R.S.: A calculus of functions for program derivation. Monograph PRG-64, Programming Research Group, University of Oxford (1987)

    Google Scholar 

  33. Bird, R.S.: Lectures on constructive functional programming. Monograph PRG-69, Programming Research Group, University of Oxford (1988)

    Google Scholar 

  34. Bird, R.S.: Unfolding pointer algorithms. J. Funct. Program. 11(3), 347–358 (2001). https://doi.org/10.1017/S0956796801003914

    Article  MATH  Google Scholar 

  35. Bird, R.S., de Moor, O.: Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Hoboken (1997)

    Google Scholar 

  36. 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

  37. Blikle, A.: Iterative systems: An algebraic approach. Bulletin de l’Académie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques XX(1) (1972)

    Google Scholar 

  38. Boom, H.: Further thoughts on Abstracto. Working Paper ELC-9, IFIP WG2.1 (1981)

    Google Scholar 

  39. 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

  40. 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

  41. 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äuser, pp. 353–372 (1996) . https://doi.org/10.1007/978-1-4612-1986-6_17

  42. 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)

    Google Scholar 

  43. 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–546 (1974)

    Google Scholar 

  44. Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552–593 (2013)

    Article  MathSciNet  Google Scholar 

  45. Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: International Conference on Functional Programming, pp. 133–144 (2013)

    Google Scholar 

  46. 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

  47. 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–53 (1983)

    Google Scholar 

  48. Burge, W.H.: Recursive Programming Techniques. Addison-Wesley, Boston (1975)

    Google Scholar 

  49. Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44–67 (1977)

    Article  MathSciNet  Google Scholar 

  50. 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–13 (2005). https://doi.org/10.1145/1040305.1040306

  51. Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000). https://doi.org/10.1007/10722010_4

    Chapter  Google Scholar 

  52. Cooper, D.: The equivalence of certain computations. Comput. J. 9, 45–52 (1966)

    Article  MathSciNet  Google Scholar 

  53. Dagand, P.E., et al.: A cosmology of datatypes: Reusability and dependent types. Ph.D. thesis, University of Strathclyde (2013)

    Google Scholar 

  54. Dang, H., Möller, B.: Concurrency and local reasoning under reverse exchange. Sci. Comput. Programm. 85, Part B, 204–223 (2013)

    Google Scholar 

  55. Dang, H., Möller, B.: Extended transitive separation logic. J. Logical Algebraic Meth. Programm. 84(3), 303–325 (2015). https://doi.org/10.1016/j.jlamp.2014.12.002

    Article  MathSciNet  MATH  Google Scholar 

  56. Dang, H., Höfner, P., Möller, B.: Algebraic separation logic. J. Logic Algebraic Programm. 80(6), 221–247 (2011). https://doi.org/10.1016/j.jlap.2011.04.003

    Article  MathSciNet  MATH  Google Scholar 

  57. Danielsson, N.A.: Functional program correctness through types. Ph.D. thesis, Chalmers University of Technology and Gothenburg University (2007)

    Google Scholar 

  58. Danielsson, N.A.: Total parser combinators. In: International Conference on Functional Programming, pp. 285–296 (2010)

    Google Scholar 

  59. Danielsson, N.A.: Correct-by-construction pretty-printing. In: Workshop on Dependently-Typed Programming, pp. 1–12 (2013)

    Google Scholar 

  60. Desharnais, J., Möller, B.: Non-associative Kleene algebra and temporal logics. In: Höfner, P., Pous, D., Struth, G. (eds.) Relational and Algebraic Methods in Computer Science. Lecture Notes in Computer Science, vol. 10226, pp. 93–108 (2017). https://doi.org/10.1007/978-3-319-57418-9_6

  61. Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Mayr, E.W., Mitchell, J.C., Lévy, J.J. (eds.) Exploring New Frontiers of Theoretical Informatics, pp. 647–660, Kluwer (2004)

    Google Scholar 

  62. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798–833 (2006)

    Article  MathSciNet  Google Scholar 

  63. Desharnais, J., Möller, B., Tchier, F.: Kleene under a modal demonic star. J. Logic Algebraic Programm. 66(2), 127–160 (2006). https://doi.org/10.1016/j.jlap.2005.04.006

    Article  MathSciNet  MATH  Google Scholar 

  64. Dewar, R.: Letter to members of IFIP WG2.1 (1977). http://ershov-arc.iis.nsk.su/archive/eaindex.asp?did=29067

  65. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Hoboken (1976)

    MATH  Google Scholar 

  66. 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–236. Springer (2000). https://doi.org/10.1007/3-540-47797-7_6

  67. Feather, M.S.: A system for developing programs by transformation. Ph.D thesis, University of Edinburgh, UK (1979). http://hdl.handle.net/1842/7296

  68. Feather, M.S.: A system for assisting program transformation. ACM Trans. Programm. Lang. 4(1), 1–20 (1982). https://doi.org/10.1145/357153.357154

    Article  MATH  Google Scholar 

  69. 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–195 (1987)

    Google Scholar 

  70. 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–32 (1967)

    Google Scholar 

  71. Fokkinga, M.: Tupling and mutumorphisms. The Squiggolist 1(4), 81–82 (1990)

    Google Scholar 

  72. Brooks, J.F.: The Mythical Man-Month. Addison-Wesley, Boston (1975)

    Google Scholar 

  73. Geurts, L., Meertens, L.: Remarks on Abstracto. Algol. Bull. 42, 56–63 (1978)

    Google Scholar 

  74. Geurts, L., Meertens, L., Pemberton, S.: The ABC Programmer’s Handbook. Prentice-Hall, Hoboken, iSBN 0-13-000027-2 (1990)

    Google Scholar 

  75. Gibbons, J.: Free delivery (functional pearl). In: Haskell Symposium, pp. 45–50 (2016). https://doi.org/10.1145/2976002.2976005

  76. 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)

    Google Scholar 

  77. Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: International Conference on Functional Programming, pp. 2–14 (2011). https://doi.org/10.1145/2034773.2034777

  78. Gibbons, J., dos Santos Oliveira, B.C.: The essence of the iterator pattern. J. Funct. Programm. 19(3,4), 377–402 (2009). https://doi.org/10.1017/S0956796809007291

  79. Gibbons, J., Henglein, F., Hinze, R., Wu, N.: Relational algebra by way of adjunctions. Proc. ACM Programm. Lang. 2(ICFP), 86:1–86:28 (2018). https://doi.org/10.1145/3236781

  80. Gomes, V.B.F., Guttmann, W., Höfner, P., Struth, G., Weber, T.: Kleene algebras with domain. Archive of Formal Proofs (2016). http://isa-afp.org/entries/KAD.html

  81. Green, C., et al.: Research on knowledge-based programming and algorithm design. Technical report Kes.U.81.2, Kestrel Institute (1981, revised 1982) (1981)

    Google Scholar 

  82. Guttmann, W.: Infinite executions of lazy and strict computations. J. Logical Algebraic Meth. Programm. 84(3), 326–340 (2015). https://doi.org/10.1016/j.jlamp.2014.08.001

    Article  MathSciNet  MATH  Google Scholar 

  83. Guttmann, W.: Stone algebras. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Stone_Algebras.html

  84. Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theoret. Comput. Sci. 744, 37–55 (2018)

    Article  MathSciNet  Google Scholar 

  85. 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

    Article  Google Scholar 

  86. Hagino, T.: A categorical programming language. Ph.D thesis, University of Edinburgh, UK (1987)

    Google Scholar 

  87. Hehner, E.C.R.: Predicative programming, part I. Commun. ACM 27(2), 134–143 (1984). https://doi.org/10.1145/69610.357988

    Article  MathSciNet  MATH  Google Scholar 

  88. Hehner, E.C.R.: Predicative programming, part II. Commun. ACM 27(2), 144–151 (1984). https://doi.org/10.1145/69610.357990

    Article  MathSciNet  MATH  Google Scholar 

  89. Hehner, E.C.R.: A Practical Theory of Programming. Springer (1993). https://doi.org/10.1007/978-1-4419-8596-5_7

  90. Hehner, E.C.R.: Specifications, programs, and total correctness. Sci. Comput. Program. 34(3), 191–205 (1999). https://doi.org/10.1016/S0167-6423(98)00027-6

    Article  MathSciNet  MATH  Google Scholar 

  91. Hinze, R.: Polytypic values possess polykinded types. Sci. Comput. Program. 43(2–3), 129–159 (2002)

    Article  MathSciNet  Google Scholar 

  92. Hinze, R.: Adjoint folds and unfolds–an extended study. Sci. Comput. Program. 78(11), 2108–2159 (2013). https://doi.org/10.1016/j.scico.2012.07.011

    Article  Google Scholar 

  93. Hinze, R., Wu, N.: Unifying structured recursion schemes: an extended study. J. Funct. Program. 26, 47 (2016)

    Article  MathSciNet  Google Scholar 

  94. Hinze, R., Jeuring, J., Löh, A.: Type-indexed data types. Sci. Comput. Program. 51(1–2), 117–151 (2004)

    Article  MathSciNet  Google Scholar 

  95. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259

    Article  MATH  Google Scholar 

  96. Hoare, C.A.R.: Programs are predicates. Philosophical Transactions of the Royal Society of London (A 312), 475–489 (1984)

    Google Scholar 

  97. Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672–686 (1987). https://doi.org/10.1145/27651.27653

    Article  MathSciNet  MATH  Google Scholar 

  98. Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Logic Algebraic Programm. 80(6), 266–296 (2011). https://doi.org/10.1016/j.jlap.2011.04.005

    Article  MathSciNet  MATH  Google Scholar 

  99. Höfner, P., Möller, B.: Algebraic neighbourhood logic. J. Logic Algebraic Programm. 76, 35–59 (2008)

    Article  MathSciNet  Google Scholar 

  100. Höfner, P., Möller, B.: An algebra of hybrid systems. J. Logic Algebraic Programm. 78, 74–97 (2009). https://doi.org/10.1016/j.jlap.2008.08.005

    Article  MathSciNet  MATH  Google Scholar 

  101. Höfner, P., Möller, B.: Fixing Zeno gaps. Theoret. Comput. Sci. 412(28), 3303–3322 (2011). https://doi.org/10.1016/j.tcs.2011.03.018

    Article  MathSciNet  MATH  Google Scholar 

  102. Höfner, P., Möller, B.: Dijkstra, Floyd and Warshall meet Kleene. Formal Aspects Comput. 24(4–6), 459–476 (2012). https://doi.org/10.1007/s00165-012-0245-4

    Article  MathSciNet  MATH  Google Scholar 

  103. Höfner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_19

    Chapter  MATH  Google Scholar 

  104. Höfner, P., Struth, G.: Non-termination in idempotent semirings. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2008. LNCS, vol. 4988, pp. 206–220. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78913-0_16

    Chapter  MATH  Google Scholar 

  105. Höfner, 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–66. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_5

    Chapter  MATH  Google Scholar 

  106. Höfner, P., Khédri, R., Möller, B.: Supplementing product families with behaviour. Softw. Inform. 5(1–2), 245–266 (2011)

    Google Scholar 

  107. Hutton, G., Meijer, E.: Monadic parsing in Haskell. J. Funct. Program. 8(4), 437–444 (1998). https://doi.org/10.1017/S0956796898003050

    Article  MATH  Google Scholar 

  108. Ionescu, C.: Vulnerability modelling with functional programming and dependent types. Math. Struct. Comput. Sci. 26(1), 114–128 (2016). https://doi.org/10.1017/S0960129514000139

    Article  MathSciNet  MATH  Google Scholar 

  109. Ionescu, C., Jansson, P.: Dependently-typed programming in scientific computing. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 140–156. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41582-1_9

    Chapter  Google Scholar 

  110. Ionescu, C., Jansson, P.: Testing versus proving in climate impact research. In: TYPES 2011, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 19, pp. 41–54 (2013). https://doi.org/10.4230/LIPIcs.TYPES.2011.41

  111. Jansson, P., Jeuring, J.: PolyP – a polytypic programming language extension. In: Principles of Programming Languages, pp. 470–482 (1997)

    Google Scholar 

  112. 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–88 (2009)

    Google Scholar 

  113. 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–56 (1991). https://doi.org/10.1109/KBSE.1991.638020

  114. von Karger, B., Berghammer, R.: A relational model for temporal logic. Logic J. IGPL 6, 157–173 (1998)

    Article  MathSciNet  Google Scholar 

  115. Ko, H.S.: Analysis and synthesis of inductive families. DPhil thesis, Oxford University, UK (2014)

    Google Scholar 

  116. Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)

    Article  Google Scholar 

  117. Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

  118. Lämmel, R., Jones, S.P.: Scrap your boilerplate: a practical design pattern for generic programming. In: Types in Language Design and Implementation, pp. 26–37 (2003)

    Google Scholar 

  119. Löh, A., Clarke, D., Jeuring, J.: Dependency-style generic Haskell. In: Shivers, O. (ed.) International Conference on Functional Programming. ACM Press, pp. 141–152 (2003)

    Google Scholar 

  120. London, P., Feather, M.: Implementing specification freedoms. Sci. Comput. Program. 2(2), 91–131 (1982)

    Article  Google Scholar 

  121. Macedo, H., Oliveira, J.N.: A linear algebra approach to OLAP. Formal Aspects Comput. 27(2), 283–307 (2015). https://doi.org/10.1007/s00165-014-0316-9

    Article  MathSciNet  MATH  Google Scholar 

  122. Magalhães, J.P., Dijkstra, A., Jeuring, J., Löh, A.: A generic deriving mechanism for Haskell. In: Haskell Symposium, pp. 37–48 (2010)

    Google Scholar 

  123. Magalhães, J.P.R.: Less is more: generic programming theory and practice. PhD thesis, Utrecht University, Netherlands (2012)

    Google Scholar 

  124. Magnusson, L., Nordström, B.: The ALF proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 213–237. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58085-9_78

    Chapter  Google Scholar 

  125. Malcolm, G.: Algebraic data types and program transformation. PhD thesis, University of Groningen (1990)

    Google Scholar 

  126. Malcolm, G.: Data structures and program transformation. Sci. Comput. Program. 14, 255–279 (1990)

    Article  MathSciNet  Google Scholar 

  127. Manna, Z., Waldinger, R.J.: Synthesis: dreams \(\rightarrow \) programs. IEEE Trans. Software Eng. 5(4), 294–328 (1979). https://doi.org/10.1109/TSE.1979.234198

    Article  MATH  Google Scholar 

  128. Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980). https://doi.org/10.1145/357084.357090

    Article  MATH  Google Scholar 

  129. Manna, Z., Waldinger, R.J.: The Deductive Foundations of Computer Programming. Addison-Wesley, Boston (1993)

    Google Scholar 

  130. Martin-Löf, P.: Constructive mathematics and computer programming. In: Studies in Logic and the Foundations of Mathematics, vol. 104, Elsevier, pp. 153–175 (1982)

    Google Scholar 

  131. 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–309 (2014). https://doi.org/10.1145/2628136.2628163

  132. McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69–111 (2004)

    Article  MathSciNet  Google Scholar 

  133. McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008). https://doi.org/10.1017/S0956796807006326

    Article  MATH  Google Scholar 

  134. McKinna, J., Wright, J.: A type-correct, stack-safe, provably correct, expression compiler in Epigram, unpublished draft (2006)

    Google Scholar 

  135. Meertens, L.: Abstracto 84: The next generation. In: Proceedings of the 1979 Annual Conference. ACM, pp. 33–39 (1979)

    Google Scholar 

  136. 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–334 (1986). https://ir.cwi.nl/pub/20634

  137. Meertens, L.: An Abstracto reader prepared for IFIP WG 2.1. Technical report CS-N8702, CWI, Amsterdam (1987)

    Google Scholar 

  138. Meertens, L.: Squiggol versus Squigol, private email to JG (2019)

    Google Scholar 

  139. Meertens, L.G.L.T.: Paramorphisms. Formal Aspects Comput. 4(5), 413–424 (1992)

    Article  Google Scholar 

  140. 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–144 (1991). https://doi.org/10.1007/3540543961_7

  141. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)

    Article  MathSciNet  Google Scholar 

  142. Möller, B.: Calculating with pointer structures. In: IFIP TC2/WG 2.1 Working Conference on Algorithmic Languages and Calculi, pp. 24–48. Chapman & Hall (1997)

    Google Scholar 

  143. Möller, B.: Kleene getting lazy. Sci. Comput. Program. 65, 195–214 (2007)

    Article  MathSciNet  Google Scholar 

  144. Möller, B.: Modal knowledge and game semirings. Comput. J. 56(1), 53–69 (2013). https://doi.org/10.1093/comjnl/bxs140

    Article  Google Scholar 

  145. Möller, B.: Geographic wayfinders and space-time algebra. J. Logical Algebraic Meth. Programm. 104, 274–302 (2019). https://doi.org/10.1016/j.jlamp.2019.02.003

    Article  MathSciNet  MATH  Google Scholar 

  146. Möller, B., Roocks, P.: An algebra of database preferences. J. Logical Algebraic Meth. Programm. 84(3), 456–481 (2015). https://doi.org/10.1016/j.jlamp.2015.01.001

    Article  MathSciNet  MATH  Google Scholar 

  147. Möller, B., Struth, G.: Modal Kleene algebra and partial correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 379–393. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27815-3_30

    Chapter  MATH  Google Scholar 

  148. Möller, B., Struth, G.: wp Is wlp. In: MacCaull, W., Winter, W., Düntsch, I. (eds.) Relational Methods in Computer Science. Lecture Notes in Computer Science, vol. 3929, pp. 200–211. Springer (2005). https://doi.org/10.1007/11734673_16

  149. Möller, B., Partsch, H., Pepper, P.: Programming with transformations: an overview of the Munich CIP project (1983)

    Google Scholar 

  150. Möller, B., Höfner, P., Struth, G.: Quantales and temporal logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 263–277. Springer, Heidelberg (2006). https://doi.org/10.1007/11784180_21

    Chapter  MATH  Google Scholar 

  151. Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10(3), 403–419 (1988). https://doi.org/10.1145/44501.44503

    Article  MATH  Google Scholar 

  152. Morgan, C.: Programming from Specifications. Prentice Hall, Hoboken (1990)

    MATH  Google Scholar 

  153. Morgan, C.: An old new notation for elementary probability theory. Sci. Comput. Program. 85, 115–136 (2014). https://doi.org/10.1016/j.scico.2013.09.003. special Issue on Mathematics of Program Construction 2012

  154. Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287–306 (1987)

    Article  MathSciNet  Google Scholar 

  155. Morris, P.W.: Constructing universes for generic programming. PhD thesis, University of Nottingham, UK (2007)

    Google Scholar 

  156. 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–579 (2009)

    Article  MathSciNet  Google Scholar 

  157. Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: International Conference on Functional Programming, pp. 62–73 (2006)

    Google Scholar 

  158. Naur, P.: The IFIP working group on ALGOL. ALGOL Bull. (Issue 15), 52 (1962)

    Google Scholar 

  159. Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)

    Google Scholar 

  160. O’Hearn, P.: Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375, 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  161. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  162. Paige, R.: Transformational programming – Applications to algorithms and systems. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Principles of Programming Languages. ACM, pp. 73–87 (1983). https://doi.org/10.1145/567067.567076

  163. 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–78 (2002)

    Google Scholar 

  164. Park, D.: On the semantics of fair parallelism. In: Bjøorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10007-5_47

    Chapter  Google Scholar 

  165. 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–35 (1983). https://doi.org/10.1016/0167-6423(83)90002-3

    Article  MathSciNet  MATH  Google Scholar 

  166. Partsch, H.: Structuring transformational developments: a case study based on Earley’s recognizer. Sci. Comput. Program. 4(1), 17–44 (1984). https://doi.org/10.1016/0167-6423(84)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  167. Partsch, H.: Transformational derivation of parsing algorithms executable on parallel architectures. In: Ammann. U. (ed.) Programmiersprachen und Programmentwicklung, Informatik-Fachberichte, vol. 77, pp. 41–57. Springer (1984). https://doi.org/10.1007/978-3-642-69393-9_3

  168. Partsch, H.: Transformational program development in a particular program domain. Sci. Comput. Program. 7(2), 99–241 (1986). https://doi.org/10.1016/0167-6423(86)90008-0

    Article  MathSciNet  MATH  Google Scholar 

  169. Partsch, H.: Specification and Transformation of Programs – A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer (1990). https://doi.org/10.1007/978-3-642-61512-2

  170. Partsch, H., Steinbrüggen, R.: Program transformation systems. ACM Comput. Surv. 15(3), 199–236 (1983)

    Article  MathSciNet  Google Scholar 

  171. Peirce, C.S.: Description of a notation for the logic of relatives, resulting from an amplification of the conceptions of Boole’s calculus of logic. Memoirs Am. Acad. Arts Sci. 9, 317–378 (1870)

    Google Scholar 

  172. Pepper, P., Smith, D.R.: A high-level derivation of global search algorithms (with constraint propagation). Sci. Comput. Program. 28(2–3), 247–271 (1997). https://doi.org/10.1016/S0167-6423(96)00023-8

    Article  Google Scholar 

  173. 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)

    Google Scholar 

  174. 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ämmel, R., Saraiva, J., Zaytsev, V. (eds.) GTTSE 2015. LNCS, vol. 10223, pp. 215–222. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60074-1_9

    Chapter  Google Scholar 

  175. Pretnar, M.: The logic and handling of algebraic effects. PhD thesis, School of Informatics, University of Edinburgh (2010)

    Google Scholar 

  176. Python Software Foundation: Python website (1997). https://www.python.org/

  177. 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–122 (2008)

    Google Scholar 

  178. Yakushev, A.R., Holdermans, S., Löh, 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–244 (2009)

    Google Scholar 

  179. Ruehr, F.: Dr Seuss on parser monads (2001). https://willamette.edu/~fruehr/haskell/seuss.html

  180. Schröder, E.: Vorlesungen über die Algebra der Logik, vol 3. Taubner (1895)

    Google Scholar 

  181. Schuman, S.A. (ed.): New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d’Informatique et d’Automatique (1975)

    Google Scholar 

  182. Schuman, S.A. (ed.): New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d’Informatique et d’Automatique (1976)

    Google Scholar 

  183. Sintzoff, M.: On the design of correct and optimal dynamical systems and games. Inf. Process. Lett. 88(1–2), 59–65 (2003). https://doi.org/10.1016/S0020-0190(03)00387-9

    Article  MathSciNet  MATH  Google Scholar 

  184. 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–359. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70594-9_18

    Chapter  MATH  Google Scholar 

  185. Smith, D.R.: KIDS: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024–1043 (1990). https://doi.org/10.1109/32.58788

    Article  Google Scholar 

  186. Spivey, J.M.: A functional theory of exceptions. Sci. Comput. Program. 14(1), 25–42 (1990). https://doi.org/10.1016/0167-6423(90)90056-J

    Article  MATH  Google Scholar 

  187. Swierstra, S.D., de Moor, O.: Virtual data structures. In: Möller, B., Partsch, H., Schuman, S. (eds.) Formal Program Development. LNCS, vol. 755, pp. 355–371. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57499-9_26

    Chapter  Google Scholar 

  188. 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–207. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61628-4_7

    Chapter  Google Scholar 

  189. Swierstra, W.: A functional specification of effects. PhD thesis, University of Nottingham (2008)

    Google Scholar 

  190. Swierstra, W., Alpuim, J.: From proposition to program. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 29–44. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29604-3_3

    Chapter  Google Scholar 

  191. Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Haskell Workshop, pp. 25–36 (2007). http://doi.acm.org/10.1145/1291201.1291206

  192. Swierstra, W., Baanen, T.: A predicate transformer semantics for effects (functional pearl). Proc. ACM Programm. Lang. 3(ICFP), 1–26 (2019)

    Google Scholar 

  193. Tafliovich, A., Hehner, E.C.R.: Quantum predicative programming. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 433–454. Springer, Heidelberg (2006). https://doi.org/10.1007/11783596_25

    Chapter  Google Scholar 

  194. Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941). https://doi.org/10.2307/2268577

    Article  MathSciNet  MATH  Google Scholar 

  195. Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10(1), 5–26 (1999)

    MathSciNet  MATH  Google Scholar 

  196. Uustalu, T., Vene, V.: Comonadic notions of computation. Electron. Notes Theoer. Comput. Sci. 203(5), 263–284 (2008). https://doi.org/10.1016/j.entcs.2008.05.029

    Article  MathSciNet  MATH  Google Scholar 

  197. Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nordic J. Comput. 8(3), 366–390 (2001)

    MathSciNet  MATH  Google Scholar 

  198. Wadler, P.: Comprehending monads. In: LISP and Functional Programming. ACM, pp. 61–78 (1990). https://doi.org/10.1145/91556.91592

  199. Wadler, P.: The essence of functional programming. In: Principles of Programming Languages. ACM, pp. 1–14 (1992). https://doi.org/10.1145/143165.143169

  200. Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)

    Article  Google Scholar 

  201. Wile, D.: POPART: producer of parsers and related tools: System builder’s manual. USC/ISI Information Science Institute, University of Southern California, Technical report (1981)

    Google Scholar 

  202. Wile, D.: Program developments as formal objects. USC/ISI Information Science Institute, University of Southern California, Technical report (1981)

    Google Scholar 

  203. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Principles of Programming Languages, pp. 214–227 (1999)

    Google Scholar 

Download references

Acknowledgements

Section 2 is based on a paper more specifically about the evolution of the Bird–Meertens Formalism [76], Sect. 3 partly based on a paper about the contributions to generic programming of the Software Technology group at Utrecht University [112], and Sect. 4 partly based on a paper about the unification of recursion schemes [93].

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Carroll Morgan .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2021 IFIP International Federation for Information Processing

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bird, R. et al. (2021). Algorithmics. In: Goedicke, M., Neuhold, E., Rannenberg, K. (eds) Advancing Research in Information and Communication Technology. IFIP Advances in Information and Communication Technology(), vol 600. Springer, Cham. https://doi.org/10.1007/978-3-030-81701-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-81701-5_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-81700-8

  • Online ISBN: 978-3-030-81701-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics