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.)
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aarts, C., et al.: Fixed-point calculus. Inf. Process. Lett. 53(3), 131–136 (1995)
Agresti, W.M.: What are the new paradigms? In: Agresti, W.M. (ed.) New Paradigms for Software Development. IEEE Computer Society Press (1986)
Alpuim, J., Swierstra, W.: Embedding the refinement calculus in Coq. Sci. Comput. Program. 164, 37–48 (2018)
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
Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013). http://isa-afp.org/entries/Kleene_Algebra.html
Armstrong, A., Foster, S., Struth, G., Weber, T.: Relation algebra. Archive of Formal Proofs (2014). http://isa-afp.org/entries/Relation_Algebra.html
Augustsson, L.: Cayenne - a language with dependent types. In: International Conference on Functional Programming, ICFP 1998, pp. 239–250 (1998)
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)
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
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
Backhouse, R.: An exploration of the Bird-Meertens formalism. Technical report CS 8810, Department of Computer Science, Groningen University (1988)
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)
Backhouse, R., Chisholm, P., Malcolm, G., Saaman, E.: Do-it-yourself type theory. Formal Aspects Comput. 1(1), 19–84 (1989)
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
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
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
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
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)
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)
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
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)
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)
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
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
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
Bemer, R.: A politico-social history of ALGOL. In: Annual Review of Automatic Programming 5, pp. 151–237. Pergamon Press, Oxford (1969)
Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic J. Comput. 10(4), 265–289 (2003)
Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects Comput. 11(2), 200–222 (1999). https://doi.org/10.1007/s001650050047
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)
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)
Bird, R.S.: An introduction to the theory of lists. Monograph PRG-56, Programming Research Group, University of Oxford (1986)
Bird, R.S.: A calculus of functions for program derivation. Monograph PRG-64, Programming Research Group, University of Oxford (1987)
Bird, R.S.: Lectures on constructive functional programming. Monograph PRG-69, Programming Research Group, University of Oxford (1988)
Bird, R.S.: Unfolding pointer algorithms. J. Funct. Program. 11(3), 347–358 (2001). https://doi.org/10.1017/S0956796801003914
Bird, R.S., de Moor, O.: Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Hoboken (1997)
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
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)
Boom, H.: Further thoughts on Abstracto. Working Paper ELC-9, IFIP WG2.1 (1981)
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
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
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
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)
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)
Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552–593 (2013)
Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: International Conference on Functional Programming, pp. 133–144 (2013)
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
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)
Burge, W.H.: Recursive Programming Techniques. Addison-Wesley, Boston (1975)
Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44–67 (1977)
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
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
Cooper, D.: The equivalence of certain computations. Comput. J. 9, 45–52 (1966)
Dagand, P.E., et al.: A cosmology of datatypes: Reusability and dependent types. Ph.D. thesis, University of Strathclyde (2013)
Dang, H., Möller, B.: Concurrency and local reasoning under reverse exchange. Sci. Comput. Programm. 85, Part B, 204–223 (2013)
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
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
Danielsson, N.A.: Functional program correctness through types. Ph.D. thesis, Chalmers University of Technology and Gothenburg University (2007)
Danielsson, N.A.: Total parser combinators. In: International Conference on Functional Programming, pp. 285–296 (2010)
Danielsson, N.A.: Correct-by-construction pretty-printing. In: Workshop on Dependently-Typed Programming, pp. 1–12 (2013)
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
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)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798–833 (2006)
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
Dewar, R.: Letter to members of IFIP WG2.1 (1977). http://ershov-arc.iis.nsk.su/archive/eaindex.asp?did=29067
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Hoboken (1976)
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
Feather, M.S.: A system for developing programs by transformation. Ph.D thesis, University of Edinburgh, UK (1979). http://hdl.handle.net/1842/7296
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
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)
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)
Fokkinga, M.: Tupling and mutumorphisms. The Squiggolist 1(4), 81–82 (1990)
Brooks, J.F.: The Mythical Man-Month. Addison-Wesley, Boston (1975)
Geurts, L., Meertens, L.: Remarks on Abstracto. Algol. Bull. 42, 56–63 (1978)
Geurts, L., Meertens, L., Pemberton, S.: The ABC Programmer’s Handbook. Prentice-Hall, Hoboken, iSBN 0-13-000027-2 (1990)
Gibbons, J.: Free delivery (functional pearl). In: Haskell Symposium, pp. 45–50 (2016). https://doi.org/10.1145/2976002.2976005
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)
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
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
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
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
Green, C., et al.: Research on knowledge-based programming and algorithm design. Technical report Kes.U.81.2, Kestrel Institute (1981, revised 1982) (1981)
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
Guttmann, W.: Stone algebras. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Stone_Algebras.html
Guttmann, W.: An algebraic framework for minimum spanning tree problems. Theoret. Comput. Sci. 744, 37–55 (2018)
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
Hagino, T.: A categorical programming language. Ph.D thesis, University of Edinburgh, UK (1987)
Hehner, E.C.R.: Predicative programming, part I. Commun. ACM 27(2), 134–143 (1984). https://doi.org/10.1145/69610.357988
Hehner, E.C.R.: Predicative programming, part II. Commun. ACM 27(2), 144–151 (1984). https://doi.org/10.1145/69610.357990
Hehner, E.C.R.: A Practical Theory of Programming. Springer (1993). https://doi.org/10.1007/978-1-4419-8596-5_7
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
Hinze, R.: Polytypic values possess polykinded types. Sci. Comput. Program. 43(2–3), 129–159 (2002)
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
Hinze, R., Wu, N.: Unifying structured recursion schemes: an extended study. J. Funct. Program. 26, 47 (2016)
Hinze, R., Jeuring, J., Löh, A.: Type-indexed data types. Sci. Comput. Program. 51(1–2), 117–151 (2004)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
Hoare, C.A.R.: Programs are predicates. Philosophical Transactions of the Royal Society of London (A 312), 475–489 (1984)
Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672–686 (1987). https://doi.org/10.1145/27651.27653
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
Höfner, P., Möller, B.: Algebraic neighbourhood logic. J. Logic Algebraic Programm. 76, 35–59 (2008)
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
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
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
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
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
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
Höfner, P., Khédri, R., Möller, B.: Supplementing product families with behaviour. Softw. Inform. 5(1–2), 245–266 (2011)
Hutton, G., Meijer, E.: Monadic parsing in Haskell. J. Funct. Program. 8(4), 437–444 (1998). https://doi.org/10.1017/S0956796898003050
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
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
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
Jansson, P., Jeuring, J.: PolyP – a polytypic programming language extension. In: Principles of Programming Languages, pp. 470–482 (1997)
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)
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
von Karger, B., Berghammer, R.: A relational model for temporal logic. Logic J. IGPL 6, 157–173 (1998)
Ko, H.S.: Analysis and synthesis of inductive families. DPhil thesis, Oxford University, UK (2014)
Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60–76 (2000)
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)
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)
London, P., Feather, M.: Implementing specification freedoms. Sci. Comput. Program. 2(2), 91–131 (1982)
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
Magalhães, J.P., Dijkstra, A., Jeuring, J., Löh, A.: A generic deriving mechanism for Haskell. In: Haskell Symposium, pp. 37–48 (2010)
Magalhães, J.P.R.: Less is more: generic programming theory and practice. PhD thesis, Utrecht University, Netherlands (2012)
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
Malcolm, G.: Algebraic data types and program transformation. PhD thesis, University of Groningen (1990)
Malcolm, G.: Data structures and program transformation. Sci. Comput. Program. 14, 255–279 (1990)
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
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
Manna, Z., Waldinger, R.J.: The Deductive Foundations of Computer Programming. Addison-Wesley, Boston (1993)
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)
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
McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69–111 (2004)
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008). https://doi.org/10.1017/S0956796807006326
McKinna, J., Wright, J.: A type-correct, stack-safe, provably correct, expression compiler in Epigram, unpublished draft (2006)
Meertens, L.: Abstracto 84: The next generation. In: Proceedings of the 1979 Annual Conference. ACM, pp. 33–39 (1979)
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
Meertens, L.: An Abstracto reader prepared for IFIP WG 2.1. Technical report CS-N8702, CWI, Amsterdam (1987)
Meertens, L.: Squiggol versus Squigol, private email to JG (2019)
Meertens, L.G.L.T.: Paramorphisms. Formal Aspects Comput. 4(5), 413–424 (1992)
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
Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)
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)
Möller, B.: Kleene getting lazy. Sci. Comput. Program. 65, 195–214 (2007)
Möller, B.: Modal knowledge and game semirings. Comput. J. 56(1), 53–69 (2013). https://doi.org/10.1093/comjnl/bxs140
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
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
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
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
Möller, B., Partsch, H., Pepper, P.: Programming with transformations: an overview of the Munich CIP project (1983)
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
Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10(3), 403–419 (1988). https://doi.org/10.1145/44501.44503
Morgan, C.: Programming from Specifications. Prentice Hall, Hoboken (1990)
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
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287–306 (1987)
Morris, P.W.: Constructing universes for generic programming. PhD thesis, University of Nottingham, UK (2007)
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)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: International Conference on Functional Programming, pp. 62–73 (2006)
Naur, P.: The IFIP working group on ALGOL. ALGOL Bull. (Issue 15), 52 (1962)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)
O’Hearn, P.: Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375, 271–307 (2007)
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
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
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)
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
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
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
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
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
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
Partsch, H., Steinbrüggen, R.: Program transformation systems. ACM Comput. Surv. 15(3), 199–236 (1983)
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)
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
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)
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
Pretnar, M.: The logic and handling of algebraic effects. PhD thesis, School of Informatics, University of Edinburgh (2010)
Python Software Foundation: Python website (1997). https://www.python.org/
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)
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)
Ruehr, F.: Dr Seuss on parser monads (2001). https://willamette.edu/~fruehr/haskell/seuss.html
Schröder, E.: Vorlesungen über die Algebra der Logik, vol 3. Taubner (1895)
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)
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)
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
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
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
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
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
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
Swierstra, W.: A functional specification of effects. PhD thesis, University of Nottingham (2008)
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
Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Haskell Workshop, pp. 25–36 (2007). http://doi.acm.org/10.1145/1291201.1291206
Swierstra, W., Baanen, T.: A predicate transformer semantics for effects (functional pearl). Proc. ACM Programm. Lang. 3(ICFP), 1–26 (2019)
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
Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941). https://doi.org/10.2307/2268577
Uustalu, T., Vene, V.: Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10(1), 5–26 (1999)
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
Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nordic J. Comput. 8(3), 366–390 (2001)
Wadler, P.: Comprehending monads. In: LISP and Functional Programming. ACM, pp. 61–78 (1990). https://doi.org/10.1145/91556.91592
Wadler, P.: The essence of functional programming. In: Principles of Programming Languages. ACM, pp. 1–14 (1992). https://doi.org/10.1145/143165.143169
Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)
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)
Wile, D.: Program developments as formal objects. USC/ISI Information Science Institute, University of Southern California, Technical report (1981)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Principles of Programming Languages, pp. 214–227 (1999)
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this chapter
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)