<figure><img src="image_1.png" /></figure>

HAL
open science

Algorithmics

Richard Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, Johan Jeuring,
Lambert Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter
Swierstra, et al.

<figure><img src="image_2.png" /></figure>

To cite this version:

Richard Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, Johan Jeuring, et al. Algorithmics. Advancing Research in Information and Communication Technology, AICT-600, pp.59-98, 2021, 10.1007/978-3-030-81701-5_3. hal-03325977

HAL Id: hal-03325977

https://inria.hal.science/hal-03325977

Submitted on 25 Aug 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Algorithmics

Richard Bird¹, Jeremy Gibbons¹, Ralf Hinze², Peter Höfner³, Johan Jeuring⁴,
Lambert Meertens⁵, Bernhard Möller⁶, Carroll Morgan⁷, Tom Schrijvers⁸,
Wouter Swierstra⁴, and Nicolas Wu⁹

¹ University of Oxford {bird,jeremy.gibbons}@cs.ox.ac.uk

² Technische Universität Kaiserslautern ralf-hinze@cs.uni-kl.de

³ Australian National University peter.hoefner@anu.edu.au

⁴ Utrecht University {j.t.jeuring,w.s.swierstra}@uu.nl

⁵ lambert@kestrel.edu

⁶ Universität Augsburg bernhard.moeller@informatik.uni-augsburg.de

⁷ University of New South Wales and Data61 (CSIRO)
carroll.morgan@unsw.edu.au (corresponding author)

⁸ KU Lueven tom.schrijvers@cs.kuleuven.be

⁹ Imperial College London n.wu@imperial.ac.uk

**Abstract.**<fnref n="10" /> 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.

**Keywords:** working groups, algorithmic programming, calculi

# 1 Introduction

WG2.1 is one of the first Working Groups of IFIP, and the oldest extant: it was founded at the request of TC2, which had begun its own very first meeting only two days before [ii]. Initially the "IFIP Working Group 2.1 on ALGOL", it is now known as the

<footnote n="10">¹⁰ Roman-numbered references like [i] in this abstract refer to details given in §10.</footnote>
IFIP Working Group 2.1 on Algorithmic Languages and Calculi. [iii]

The Group has always focused on methods for systematic program construc-
tion; and our goal is to make the methods steadily more powerful and more
general. For example, the formalisation of the inductive assertion method [iv]
led to a logical method based on pre- and postconditions [v], and then to a
strongly calculational goal-directed method [vi]. Generalising programs to spe-
cial cases of specifications [vii] led to the Mathematics of Program Construction.
And a program-algebraic approach evolved from that: the “Laws of Program-
ming” [viii].

Mathematics (of program construction or otherwise) can be carried out with
pencil and paper. For programs, however, there are more significant advantages
in automation than for mathematics generally; thus the Group has always paid
attention to program transformation systems [ix] — but their design should be
based on the ‘by hand’ calculations that preceded them.

Language design, including the advancement of ALGOL, remained a main
interest for many years, focussing for a period specifically on a more advanced
language called “Abstracto”.<fnref n="11" /> Abstracto generalised what ‘programming’ lan-
guages actually *should* be: rather than just for programming or writing exe-
cutable code, they should also be able to describe algorithms in an abstract way.
They should allow expressing (initially vague) ideas about an algorithm’s high-
level structure and, after transformations adding details, reach a level from which
the final step to ‘real’ programming-language code is simple enough to minimise
the risk of transcription errors. In sum, Abstracto was supposed to support and
codify our *Algorithmics* activity: but our activity itself outgrew that.

ALGOL 60 and 68 were languages more oriented to programmers’ thoughts
than to computers’ hardware. In their ‘successor’ Abstracto, we wanted [xi]

... a programming language some of whose features we know:

1. It is very high level, whatever that means. (1)

2. It is suitable for expressing initial thoughts on construction of a program.

3. It need not be (and probably is not) executable...

Abstracto was to be an *algorithmic language*: one for describing the algorithmic
steps in a computation, not just the input-output relation or similar behavioural
specification. But it was still intended to be a ‘tool of thought’, rather than
primarily an implementation language.

But the Abstracto approach was *itself* soon abstracted by abandoning the
imperative ALGOL-like language structures, switching to a more functional pre-
sentation [xii] in which there was an algebra of programs *themselves*, rather than
say an algebra of statements *about* programs. The framework for this became
known as the “Bird–Meertens Formalism”, a very concise notation in which al-
gorithmic strategies can be expressed and transformed (§2). That exposed many

<footnote n="11">¹¹ The name is said to have come from the Latin phrase *in abstracto*, used in class by a lecturer [x] who said that he would first present an algorithm ‘in abstracto’ before developing it in ALGOL 60. At the end of the class, a student asked whether he could “learn more about this Abstracto programming language”.</footnote>
general algorithmic patterns and calculational laws about them that had, until
then, been obscured by the earlier imperative control structures.

A similar abstracting approach was applied to data structures in the form of
a hierarchy –the Boom hierarchy– leading from sets through multisets (bags) and
lists to (binary) trees [xiii] (§2.3, §3). The insight was that all these structures had
a common pattern of constructors (an empty structure, a singleton constructor,
and a binary combiner).<sup>12</sup> They were distinguished from each other not by the
signatures of their operations, but rather by the algebraic laws imposed on the
constructors: the fewer laws, the more structure in the generated elements.

A further abstraction was to allow the constructors to vary, i.e. to have an
even more general approach in which one could say rigorously "Sum the integers
in a structure, no matter what its shape." and then reason effectively about it,
for example that "Square all the integers in a structure, and then add them
up." is the same as "Sum the squares of all the integers in that structure." This
led to generic programming (§3). Genericity was achieved by using elementary
concepts from algebra and category theory — functors, initial and final algebras,
and the various kinds of morphisms on them [xiv](§4). Programs taking advan-
tage of this are called "polytypic", i.e. allowing many kinds of type structures,
in the same way that polymorphic programs allow many kinds of type values
within a single class of structures.

Unfortunately, the kind of specification that most polytypic languages sup-
port in their type signatures is very limited. Type theory [xv] however showed
how any specification expressible in predicate logic could serve as the type of a
program. That enables programmers to capture arbitrary invariants and speci-
fications of their programs, such as balanced trees or sorted lists, simply as part
of the program's type. Since types are checked at compile-time, any type-correct
program will never violate those specifications at runtime. This is supported by
dependently typed programming languages (§5).

Besides the activities around data structures there was also a branch of work
dealing with the task of mimicking imperative structures, as, e.g., necessary to
describe interaction with the environment, in a purely functional context. Mon-
ads, applicative functors, and algebraic effects have provided a mathematically
solid account that could be formulated in a way that allowed program-algebraic
calculation after all (§6).

The investigations into data structures and generic algorithms on them were
mainly carried out around (quotients of) tree-like structures. However, there are
numerous more general (graph-like) structures which are not easily represented
in that framework. As these should be approachable by calculations as well, our
activities have therefore also dealt with relational or relationally based struc-
tures, which is their natural mathematical representation. Abstracting relations
to algebraic structures such as Kleene algebras provides notions well suited for
describing not only data structures but also control structures of various kinds

<footnote n="12"><sup>12</sup> Compare the empty set `{}`, the singleton set `{x}` and set union with the empty list `[]`, the one-element list `[x]` and list concatenation.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 1. Abstracto 84 [xx]</figcaption></figure>

(§7). This approach also links nicely to the predicate transformer approaches [vi] and the “Laws of Programming” [viii].

Systematic program construction benefits greatly from program construction systems — tools to support the work of the program constructor. This work involves reasoning about programs, which can be shallow and tedious; automated tools are less error-prone than humans at such activities. Moreover, programs are usually much longer than formal expressions in other contexts, such as in traditional mathematics; so tool support is also a convenience. Finally, a system can record the development history, producing automatically the software documentation that allows a replay, upon a change of specification, or an audit if something goes wrong. The Group has always worked on design and engineering of transformation systems in parallel with the work on the underlying transformation calculi; our survey therefore concludes with a more detailed account of corresponding tool support (§8).

Generally, the Group's pattern has always been to expand the concepts that enable rigorous construction of correct programs, then streamline their application, and finally simplify their presentation. And then... expand again.

As the trajectory in this section has described (with the benefit of hindsight) the Group has always had diverse interests that arise from our program-calculational 'mindset' applied to other computer-science interest areas and even real-world contemporary problems [xvi].

# 2 From ALGOL, via Abstracto... to Squiggol

## 2.1 Abstracto: the first move towards algorithmics

After the completion of the *Revised Report on ALGOL 68* [xix], the Group set up a *Future Work* subcommittee to decide how to progress. This subcommittee in turn organised two public conferences on *New Directions in Algorithmic Languages* [xi], after which the Group focussed again on specific topics. The Chair highlighted two foci: programming languages for beginners [xvii], and “Abstracto”. The first led to the development of the beginner's language ABC and hence eventually to Python [xviii]; the other was *Abstracto*, and was

> ... not a specification language as such since it is still concerned with how to do things and not just what is to be done, but [allowing] the expression of the 'how' in the simplest and most abstract possible way. [xi]

A representative example of Abstracto is shown in Figure 1. It is part of the development of a 'fast exponentiation' algorithm: given natural numbers X and
<figure><img src="image_5.png" /><figcaption>Fig. 2. The oldest inhabitant, in Abstracto [138]</figcaption></figure>

Y, compute $z = X^Y$ using only $O(\log_2 Y)$ iterations. The program on the left shows a 'while' loop, with invariant $z \times x^y = X^Y$, variant $y$, and guard $y \neq 0$. The program on the right factors out $r = y \mod 2$, refining the nondeterminism in the first program to a deterministic loop. Thus our vision for Abstracto was as a kind of 'refinement calculus' for imperative programs. [xxi]

## 2.2 The Bird–Meertens Formalism (BMF): a higher-level approach

Although the Abstracto approach was successful, in the sense that it could be used to solve the various challenge problems that the Group worked on, after some time it was realised that the transformation steps needed were too low level — and so a key insight was to lift the reasoning to a higher level [xxii], namely to abandon the imperative ALGOL-like style and the corresponding refinement-oriented approach of Abstracto, and to switch instead to a more algebraic, functional presentation.

It made a big difference. Consider for example the two programs in Figure 2 [xx], where the problem is to find the (assumed unique) oldest inhabitant of the Netherlands. The data is given by a collection *dm* of Dutch municipalities, and an array *mr*[-] of municipal registers of individuals, one register per municipality. The program on the left combines all the municipal registers into one national register; the program on the right finds the oldest inhabitant of each municipality, and then findest the oldest among those ‘local Methuselahs’. Provided that no municipality uninhabited, the two programs have equivalent behaviour. However, one cannot reasonably expect that precise transformation, from the one to the other, to be present in any catalogue of transformations. Instead, the development should proceed by a series of simpler steps that, because of their
<figure><img src="image_6.png" /><figcaption>Fig. 3. The Maximum Segment Sum problem [xxiv]</figcaption></figure>

simplicity, can feasibly be collected in a smaller and more manageable catalogue of general-purpose transformations.

The equivalent higher-level transformation is this one: [xxii]

$$ \uparrow_{age} / +/mr \cdot dm = \uparrow_{age} / (\uparrow_{age} / mr) \cdot dm $$

Its left-hand side takes the oldest in the union of the registers of each of the municipalities, and the right-hand side takes the oldest among those local Methuselahs. The “⊕/” reduces a collection using binary operator ⊕; the “+” is binary union; the “↑f” chooses which of two arguments has the greater f-value; the “g*” maps function g over a collection; and finally, function composition is indicated

by juxtaposition. The functional presentation is clearly an order of magnitude shorter than the Abstracto one. It is also easier to see what form the small general-purpose transformation steps should take — simple equations such as “reduce promotion” (⊕/ +/ = ⊕/ ⊕/*) and “map fusion” (f* g* = (fg)*) [xxiii]. The notation evolved further through the 1980’s [xxiv], and came to be known as “Squiggol”. It was later given the more respectable name “Bird–Meertens Formalism” [xxv], and inspired the Group’s further efforts in rigorous, concise program development.

<figure><img src="image_7.png" /></figure>

Let us calculate!

Another example of concise calculation is given in Fig. 3.

## 2.3 The Boom Hierarchy of data structures

The operators and transformation rules of Squiggol/BMF apply equally to lists, bags, and sets. And those three datatypes are conceptually linked by their common signature of constructors (an empty structure, a singleton constructor, and a binary combination) but satisfying different laws (associativity, commutativity, and idempotence of the binary combination, with the empty structure as a
unit). Moreover, the core operations (maps, filters, and reductions) are homomorphisms over this algebraic structure.

Crucially, each datatype is the *free algebra* on that common signature, with a given set of equations, generated from a domain of individual elements; that is, there exists a *unique* homomorphism from the datatype to any other algebra of the same kind. For example, writing “[]” for the empty structure, “[x]” for a singleton, “+” for the binary combination, and given a binary operator ⊕ with unit e, the three equations

$$ 
\begin{align*}
\oplus/[] &= e \\
\oplus/[a] &= a \\
\oplus/(x + y) &= \oplus/x \oplus \oplus/y
\end{align*}
$$

determine the reduction operator ⊕/ uniquely: provided that ⊕ is associative, these three equations have as their unique solution the aggregation function from lists. But if we add the assumption that ⊕ is also commutative, then there is a unique function from bags; and if we add idempotence, then there is a unique function from sets.

If out of curiosity we assert *no* equations of the binary operator alone, only that the empty structure is its unit, then we obtain a fourth member of the family, a peculiar sort of binary tree. The four members form a hierarchy, by adding the three equations one by one to this tree type. The resulting hierarchy of data structures was called the “Boom” hierarchy [xiii]. Its connections to the Eindhoven quantifier notation [xxvi] greatly simplified the body of operators and laws needed for a useful theory.

## 3 Generic programming: function follows form

The Boom hierarchy is an example of how we can use algebras and homomorphisms to describe a collection of datatypes, together with a number of basic operations on those datatypes. In the case of the Boom hierarchy, the constructors of the algebra are fixed, and the laws the operators satisfy vary. Another axis along which we can abstract is the *constructors* of a datatype: we realised that concepts from category theory can be used to describe a large collection of datatypes as initial algebras or final coalgebras of a functor [xiv]. The action of the initial algebra represents the constructors of the datatype it models. And it has the attractive property that any homomorphism on the functor algebra induces a unique function from the initial algebra. Such a function was called a *catamorphism* [xxvii]. A catamorphism captures the canonical recursive form on a datatype represented by an initial algebra. In the functional programming world, a catamorphism is called a fold, and in object-oriented programming languages the concept corresponds closely to visitors. Typical examples are functions like map, applying an argument function to all elements in a value of a datatype, and size, returning the number of elements in a value of a (container) datatype. Catamorphisms satisfy a nice fusion property, which is the basis of many laws in programming calculi. This work started a line of research
```
flatten   :: Regular d => d a -> [a]
flatten   = cata fl
```

```
polytypic fl :: f a [a] -> [a] =
  case f of
    g + h -> either fl fl
    g * h -> \(x,y) -> fl x ++ fl y
    ()    -> \x -> []
    Par   -> \x -> [x]
    Rec   -> \x -> x
    d @ g -> concat . flatten . pmap fl
    Con t -> \x -> []
```

<caption>Fig. 4. A PolyP program to flatten a container to a list [xxix]</caption>

on *datatype-generic programming* [xxviii], capturing various forms of recursion as morphisms, more about which in §4.

The program calculus thus developed could be used to calculate solutions to many software problems. As a spin-off, the theory described programs that could be implemented in a standard, but different, way on datatypes that can be described as initial functor-algebras. No general-purpose programming language supported such typed, generic functions, so these functions had to be implemented over and again for different datatypes.

Using the structure of polynomial functors, the language PolyP was designed that extended the lazy, higher-order functional programming language Haskell [xxix]. In PolyP, a generic function is defined by means of induction on the structure of functors. Using this programming language it was possible to define not only the recursive combiners from the program calculus, such as folds and unfolds, but also to write generic programs for unification, term rewriting, pattern matching, etc. Fig. 4 shows an example of a polytypic program.

PolyP supported the definition of generic functions on datatypes that can be described as initial functor-algebras but do not involve mutual recursion. While sufficient for proof-of-concept demonstration purposes, this last restriction was a severe limitation on practical applicability. Generic programming is particularly attractive in situations with large datatypes, such as the abstract syntax of programming languages, and such datatypes are usually mutually recursive. Generic Haskell was developed to support generic functions on sets of mutually recursive datatypes [xxx]. Generic functions defined in Generic Haskell can be applied to values of almost any datatype definable in Haskell. Fig. 5 shows how a generic equality function is implemented in Generic Haskell.

The approach of defining generic functions in Generic Haskell can also be used to define type-indexed (or generic) datatypes. A type-indexed datatype is a data type that is constructed in a generic way from an argument data type.
<figure><img src="image_8.png" /><figcaption>Fig. 5. A Generic Haskell program for equality [xxx]</figcaption></figure>

For example, in the case of digital searching, we have to define a search tree type by induction on the structure of the type of search keys. Generic Haskell also supports the possibility of defining type-indexed datatypes [xxxi]. The functional programming language Haskell now supports a light-weight variant of type-indexed datatypes through type families.

The fixed-point structure of datatypes is lost in Generic Haskell, however, and with it the capability of defining the generic fold function. It was then discovered how to obtain a fixed-point representation of possibly mutually recursive datatypes, bringing the generic fold function back into the fold [xxxii]. Thus we can define the fold function for the abstract syntax of a programming language, bringing generic programming within reach of compiler writers.

Meanwhile, Haskell –or, more precisely, compilers supporting various Haskell extensions– evolved considerably since PolyP and Generic Haskell were developed. With respect to types, GHC, the Glasgow Haskell Compiler, now supports multiple-parameter type classes, generalised algebraic datatypes (GADTs), type families, etc. Using these extensions, it is now possible to define generic functions in Haskell itself, using a library for generic programming. Since 2000, tens of such libraries have been developed world-wide [xxxiii]. Since –from a generic programming perspective– the expressiveness of these libraries is almost the same as the special-purpose language extensions, and since such libraries are much easier to develop, maintain, and ship, these libraries make generic programming more generally available. Indeed, these libraries have found their way to a wider audience: for example, Scrap Your Boilerplate has been downloaded almost 300,000 times, and Generic Deriving almost 100,000 times [xxxiii].

## 4 Morphisms: suddenly they are everywhere

In §3 we identified catamorphisms as a canonical recursive form on a datatype represented by an initial algebra: in functional-programming parlance, a *fold*. From there, however, further work [xxxiv] led to a rich research agenda concerned
with capturing the pattern of many other useful recursive functions that did not quite fit that scheme, that were not *quite* 'catamorphic'. Indeed, it gave rise to a whole zoo of morphisms: *mutumorphisms*, *zygomorphisms*, *histomorphisms*, generalised folds, and generic accumulations [xxxv]. Just as with catamorphisms, those recursion schemes attracted attention because they made termination or progress manifest (no need to prove or check it) and they enjoyed many useful and general calculational properties — which would otherwise have to be established afresh for each new application.

## 4.1 Diversification

Where while-loops are governed by a predicate on the current state, and for loops by an incrementing counter, structured recursion schemes such as catamorphisms take a more restricted approach where it is the structure of the input data itself that controls the flow of execution ("function follows form").

As a simple example, consider how a list of integers is summed: a catamorphism simply recurses over the structure of the list. No for-loop index variable, and no predicate: when the list is empty the sum is zero, and when the list contains at least one number it should be added to the sum of the residual list. While-loops could easily encode such tasks, but their extra expressive power is also their weakness: we know that it is not always tractable to analyse loops in general. With catamorphisms, the analysis is much simpler — the recursion scheme is simply induction over a datatype.

The analogy with induction goes further. Number theorists have long studied computable functions on natural numbers, and an important class are the primitive recursive functions, which provide the recursive step with the original argument as well as the result of recursing on that argument. Such functions are an instance of the *paramorphism* [xxxvi], which is an interchangeable variation on the catamorphism.

Further still, an attractive variant of induction is *strong* induction, where the inductive step can rely on all the previous steps. Its parallel as a recursion scheme is the *histomorphism* and, just as strong induction and induction are interchangeable, histomorphisms are encodable as catamorphisms. The utility of these schemes –the point of it all– is however to make it convenient to describe programs that would otherwise be difficult to express, and to derive others from them. In the case of histomorphisms (strong recursion), for example, it is the essence of simple dynamic programming programs such as the knapsack problem, or counting the number of possible bracketings, that was captured. More complex dynamic programming problems, such as the multiplication of a chain of matrices, requires a slightly more nuanced recursion scheme, the *dynamorphism*, where an intermediate data structure is generated.

We recall that the exploitation of various forms of duality revolutionalised the field of physics; algorithmics similarly benefits from an important form of input-output duality. Each recursion scheme features a dual scheme: while one focuses on consuming the input, the other emphasizes producing the output. To illustrate, consider how insertion sort deconstructs a list by extracting numbers
one at a time (input), inserting them appropriately into a sorted list (output). Whereas the deconstruction of the original list is another catamorphism, the construction of the sorted list exemplifies an *anamorphism* — it is the dual situation. Thus expressing insertion sort in terms of recursion schemes allows us to dualize the algorithm to obtain another sorting algorithm *for free*: selection sort. This works by constructing a sorted list (an anamorphism), and at each step performs a selection that deconstructs the unsorted list to extract the smallest element (a paramorphism).

Another way to understand a catamorphism is that it applies a strategy that takes subsolutions and conquers them (with a so-called *algebra*) to provide a final solution. Dually, an anamorphism applies a strategy that takes a problem and splits it up into subproblems (with a so-called *coalgebra*). Those can be understood as the two components of a divide-and-conquer strategy, and the combination is known as a *hylomorphism*, depicted in the diagram below:

<figure><img src="image_9.png" /></figure>

Catamorphisms are then the special case of this diagram where the dividing step simply *deconstructs* a data structure, and anamorphisms the special case where the conquering step *constructs* a data structure.

## 4.2 Unification

The multitude of generalisations of catamorphisms and their duals is bewildering.

Many of them were defined as adaptations of catamorphisms, but in most cases showing that those corresponded directly to catamorphisms required careful calculation. And with so many different variations, a natural question is whether there is some underlying commonality that unifies them all. Indeed there is.

The unification was achieved by borrowing some slightly more sophisticated machinery from category theory. A first attempt was to use comonads, which allow access to contextual information [xxxvii], to organise the structure of recursive calls. Another attempt used adjunctions instead as the common thread [xxxviii]. That resulted in so-called “adjoint” folds, which show how a catamorphism in one category can give rise to a different recursion scheme in another. Although the two methods were initially thought to be disjoint, later work revealed recursion schemes from comonads to be a special case of adjoint folds with an appropriate distributive law.
Each of these two unifications of recursion schemes treated generalizations of catamorphisms separately to their dual counterparts of anamorphisms. But both are special cases of hylomorphisms; and so the next step was to generalise *all* inductive and coinductive recursion schemes within the single unifying theme of *conjugate hylomorphisms* — or ‘the mother of all recursion schemes’. Naturally, the Group named it the *mamamorphism*. This time, the more sophisticated categorical techniques were used to extend the work on adjoint folds with conjugate distributive laws to connect pairs of adjunctions.

All in all, the unifying work on recursion schemes benefitted greatly from the unifying power of category theory — which is what category theory is for.

# 5 Dependent types: types you can depend on

Datatype-generic programming explores how to define functions and datatypes by induction over the structure of algebraic types. This line of research within the Group sparked further interest in the exploration of how to use static type information in the construction of programs. In particular, emerging programming languages with *dependent types* offered new opportunities for program verification, program transformation, program calculation and type-directed program development.

## 5.1 What are dependent types?

The idea of programming with dependent types dates back at least as far as the 1970's, when it became increasingly clear that there was a deep connection between constructive mathematics and computer programming [xxxix]. In the late 20th century, a number of new programming languages emerged, exploring these ideas [xl]. Those languages, and their implementations, enabled the further exploration of the possibilities that statically typed languages with dependent types offered. Each of them adopted the *Curry-Howard correspondence* [xli], connecting programming languages and mathematical logic, as the guiding principle of *program language design*. The terms of each language correspond to both programs and proofs; a type can equally well be read as a specification or a proposition. To ensure the logic underlying a language's type system is *sound*, all functions must be total, disallowing partial incomplete pattern matching and diverging functions. The benefit of this disciplined approach to software development is that these languages provide a unified setting for both programming and program verification. Given the strong traditions of program calculation and functional programming within the Group, for instance, using the Bird-Meertens Formalism to perform equational reasoning about Haskell programs, there was a clear interest in these new languages. Furthermore, the richer language of algebraic data types offered the ability to enforce invariants during a program's construction.
## 5.2 Dependent types

At the beginning of the 21st century, the relation between dependently typed programming and datatype generic programming was clearly emerging [xlii] leading to several influential PhD theses on this topic. The interest in dependent types from members of the Group dates back to the late 80’s [xliii].

The new languages based on type theory reinvigorated some of the past research that members of the Group have done on the derivation of correct programs. Following the Agda tutorial at Meeting #63 [xliv], the work on relational program calculation, for example, was shown to be possible within dependently typed languages. Similarly, the refinement calculus, used to derive a program from its specification, could be embedded in a proof assistant, enabling pen and paper proofs to be machine-checked. Program calculation in the style of Dijkstra using predicate transformer semantics could be modelled using type theory, rather than the traditional impredicative set theory. Types and proof assistants based on type theory became a central tool in the calculation of correct programs [xlv].

At that point, an influx of new members broadened the Group’s interest to novel application areas for dependently typed programming [xlvi], such as scientific computation, decision problems, and even the study of climate change. Combinator parsing, previously studied in the context of functional programming (see §6.2), was implemented in a total language with dependent types [xlvii].

The new languages with dependent types also enabled new opportunities to exploit static type information to guide program development [xlviii] — in the same spirit as the research on datatype generic programming. Types can be read as a (partial) specification. The discovery of a type-correct program can arise from a dialogue with the type checker, helping establish a program’s correctness as it is written. There are numerous domain-specific languages and data types designed to enforce certain correctness properties by construction.

Dependently typed programming languages marry constructive logic and programming in a manner unfamiliar to most programmers. To ensure that the type system is sound, all programs must be total. Yet any mainstream language relies on numerous *effects*, such as general recursion, mutable state, concurrency, or exceptions, each of which break the promise of totality. To address this, there has been a line of research on how to incorporate effects in dependently typed program languages [xlix]. This, in turn, led to renewed interest from the Group on how to program safely and robustly in the presence of arbitrary side-effects in any language, resulting in the study of *algebraic effects* (see §6).

# 6 Computational effects: beyond the functional

When the Group switched to a purely functional presentation of programs [xxii], that is from Abstracto to Squiggol (§2), at first this also meant doing away with a group of programming-language features known collectively as “effects”.
## 6.1 Effects and monads

Effects cover all behavioural aspects of a computational function that go beyond the input-output behaviour of mathematical functions. It includes interaction of a program with its environment (the file system and operating system, other processes, human operators, distant servers, ...), mechanisms for structuring the internal control flow (partiality and exceptions, backtracking, nondeterminism and probability, delimited control, ...), and implicit dataflows (mutable state and global variables).

While some of these effects are indeed symptoms of a low-level imperative encoding, such as local mutable state, others are essential in real-world programs that interact with the environment. And they can be important for structuring programs compositionally: examples are exceptions and backtracking.

Fortunately, it turned out that useful effects need not be abandoned in a purely functional setting [l] — the ‘doing away with’ was only temporary. Effects can after all be modelled with pure functions. Here are some examples:

<table><tr><td>a &rarr; b</td><td>a pure function</td></tr><tr><td>a &rarr; 1 + b</td><td>a partial function</td></tr><tr><td>a &rarr; e + b</td><td>a function with exceptions e</td></tr><tr><td>a &rarr; b<sup>+</sup></td><td>a nondeterministic function</td></tr><tr><td>a &rarr; b<sup>*</sup></td><td>... which might also fail</td></tr><tr><td>a &rarr; b &times; o<sup>*</sup></td><td>a function that sends os to its environment</td></tr><tr><td>a &rarr; &mu;x.((i &rarr; x) + b)</td><td>a function that reads is from its environment</td></tr><tr><td>a &rarr; (s &rarr; (b &times; s))</td><td>a function with implicit state s</td></tr><tr><td>&vellip;</td><td></td></tr></table>

(where $b^+$ denotes non-empty sequences of $bs$, and $b^*$ possibly empty sequences).

It turned out that all those different types of functions with effects are ‘Kleisli’ arrows for appropriately structured monads [li]. The utility of the monad was that it handled calculation, in particular composition, of the types above in a single unified way. Whereas two functions of types $a \to b$ and $b \to c$ are easily composed to make a single function of type $a \to c$, it is not clear at first how to compose $a \to e+b$ and $b \to e+c$ to $a \to e+c$, or for that matter $a \to b^+$ and $b \to c^+$ to $a \to c^+$. And even when the (in retrospect) obvious definitions are adopted, one for each, the challenge is then to see those definitions as instances of a single generalised composition. That’s what Kleisli composition achieves.

## 6.2 Functions too weak, monads too strong: Applicative functors? Just right.

Once monads had brought effects back in the purview of purely functional reasoning, the Group turned its attention to reasoning about such programs — ‘effectful’ programs. One fruitful example has been the study of recursive descent parsers [lii]. They lend themselves to a combinator style of programming. Moreover, the combinators fall neatly out of the observation that the datatype
of parsers that return a parsed value is another monad, a combination of implicit state and nondeterminism with failure: the Kleisli arrows are of the form

$$a \to (\Sigma^* \to (b \times \Sigma^*)^*)$$

where the alphabet of symbols is Σ or, in verse [liii],

A parser for things
is a function from strings
to lists of pairs
of things and strings.

But the monadic presentation makes static analysis difficult: the interface allows earlier inputs to determine the parser used for later inputs, which is both more expressive than necessary (because few applications require such configurable syntax) and too expressive to analyse (because the later parser is not statically available). A weaker interface for effects turns out to be nearly as expressive, and much more amenable to analysis. The essence of this weaker interface was abstracted as an ‘applicative functor’, and has served as the foundation of significant subsequent work [liv].

## 6.3 Algebraic effects and handlers

But how to reason about effectful programs, such as applicative parsers, nonde-terministic functions, and programs that perform I/O? A first step is to treat the effectful operations as an abstract datatype, provide a purely functional specification of that data abstraction, prove the program correct with respect to the algebraic specification, but run the program against the ‘real’ implementation that incurs actual effects such as I/O. In fact, one could consider the algebraic specification as the interface in the first place, and incorporate its axioms into traditional equational reasoning; it is then the responsibility of the implementer of the effect to satisfy the axioms. This approach is cleanly formalized in the notion of *algebraic effects and handlers*, whereby a pure functional program assembles a term describing the effects to be performed, and a complementary environment *handles* the term, by analogy with handling an exception [lv]. In fact, that term is a value of a type captured as the *free monad* on the signature of the effect operations, a datatype-generic notion (see §3).

# 7 Lifting the game: A purely algebraic view of algorithms and languages

The systematic construction of algorithms –or, more generally, of computer programs– needs languages that are precise, effective, and that allow calculational reasoning. Previous sections showed how the Group discovered the striking similarities between derivations from quite different areas, such as path problems and regular languages [lvi]. Using algebra in its purest form, i.e. starting with
<table><caption>**Fig. 6.** Operators of semirings and relation algebras</caption><thead><tr><th>semiring (program interpretation)</th><th>relation algebra</th></tr></thead><tbody><tr><td>+</td><td>∪ union</td></tr><tr><td>· sequential composition</td><td>; relational composition</td></tr><tr><td>≤ refinement</td><td>⊆ subset</td></tr><tr><td>0 abort</td><td>∅ empty relation</td></tr><tr><td>1 skip</td><td>I identity relation</td></tr></tbody></table>

a collection of postulated axioms and carrying out (program) derivations based on those laws alone, therefore enables an extremely abstract treatment: those derivations are then valid in *any* programming model that satisfies the axioms.

Calculi based on the algebra of binary relations [lvii] were prime candidates for that, since they allow a natural treatment of directed graphs — and they abstract and unify data structures (e.g. trees), transition systems and many more concepts.

Also, relations are intimately connected with predicates and hence can be used to describe (by pre- and postconditions) and calculate input-output behaviour. In particular, they cover principles of algorithm design such as dynamic programming, greedy algorithms etc. [lvi]

*Relation Algebras* make relations, i.e. sets of argument-value pairs, ‘first-class citizens’ by viewing them as algebraic elements subject to operators that treat them as a whole without looking at their internal structure. The ‘point-free’ approach that this enables often admits considerable concision. The basic relational operators (Fig. 6, right) are simply set union, intersection and complement, supplemented by sequential composition.

Although a relation-algebraic approach already allows the unified treatment of different instances of graph problems [lviii], replacing sets of pairs (single relations) by other entities yields further models of the same algebraic signature, known as (*idempotent semirings*). Fig. 6 (left) shows the operators common to semirings.

And those structures have applications in programming languages, algorithms, logic and software engineering:

- *Classical logic* is a well known simple semiring, in which choice corresponds to disjunction, composition to conjunction, 0 to *false* and 1 to *true*. To subsume classical logic fully, however, one requires negation — i.e. a Boolean algebra.

- When elements of a semiring are interpreted as (arbitrary) *programs*, the basic operators represent nondeterministic choice and sequential composition; 0 corresponds to the program *abort* and 1 to *skip*. Equations such as $1 \cdot x = x = x \cdot 1$ and $0 \cdot x = 0 = x \cdot 0$ form the basis of algebraic reasoning, including program transformations. The equations describe the facts that any program *x* composed with *skip* is identical to the program itself, and that any program composed with *abort* is identical to *abort*. This allows the expression of programs and specifications in the same framework. A program
P satisfies a specification S if $P \leq S$, where $\leq$ expresses refinement, which is the canonical order available in every idempotent semiring. (In other styles of program calculation, that would be written $S \sqsubseteq P$.) This simple formulation of program correctness enables a wide range of methods for calculational program derivation and program verification [lix].

- Using partial maps as algebraic elements allows treating data structures with pointers. This usage was inspired by Squiggol (§2) [lx].

- When the underlying structure reflects the memory cells (heaps), the algebraic framework provides an abstract version of separation logic [lxi].

- When the algebraic elements are interpreted as sets of sets or sets of lists it is possible to derive aspects of feature-oriented software development, including the formal characterisation of product families and of feature interactions [lxii].

- Graphs are often equipped with edge labels representing weights, capacities or probabilities; likewise automata and labelled transition systems carry extra edge information in addition to source and target. Those can be treated by generalising Boolean matrices to matrices over other algebras. For classical graph algorithms, such as shortest-path algorithms, the max-plus algebra and the min-plus algebra are useful as underlying structure — here, min/max play the roles of (biased) choice, and plus is the operator for sequential composition (that is, adding path lengths/costs).

- Probabilistic aspects can be represented by matrices with real values between 0 and 1, and fit into the very same algebraic framework. Applications include calculational derivations of fuzzy algorithms.

- Fundamental concepts of programming-language semantics, including concurrent programs and termination, can be handled algebraically as well. Beyond the areas mentioned above, the Group has also applied this algebra in several areas, included object-oriented programming, data processing, game analysis and routing in mobile networks [lxii].

But semirings can be extended: and those extensions are used to capture additional concepts from data structures, program logics and program transformation. Here are some examples.

*Kleene algebras*, generalising the algebra of regular expressions, offer the additional operator $\cdot^*$ of arbitrary finite iteration. Algebraically, the loop while $p$ do $x$ becomes $(p \cdot x)^* \cdot \neg p$, which is the least fixed-point of the function $\lambda y$. if $p$ then $x \cdot y$ else skip [lxiii].

Here $p$ is a specific element, called a *test*, representing a predicate on the state space. The set of tests offers a negation operator $\neg$ and hence forms a Boolean algebra [lxiv]. In the interpretation where algebraic elements are programs, a test $p$ corresponds to an *assert* statement. For tests $p, q$ and program element $x$ the inequation $p \cdot x \leq q \cdot x$ algebraically expresses the Hoare triple $\{p\}x\{q\}$ [lxi].

Furthermore, in certain Kleene algebras, known as *quantales*, the principle of fixed-point fusion [lxv] is a theorem, i.e. it can be derived from the axioms. This illustrates once again the powers of 'algebraic unification'. Fusion, shown in §§ 2,3 to be an extremely practical law for transforming functional programs,
is now available for many other kinds of program too. Examples include merging of programs with the same loop structure, or ‘deforestation’, i.e. avoiding the generation of a large intermediate data structure that afterwards is ‘consumed’ again, in favour of ‘generation and consumption on the fly’. This is also known as “virtual” data structures [lxvi].

*Omega algebras* [lxvii], which offer an operator $\omega$ for infinite iteration, allow the description and analysis of systems or programs with potentially never-ending behaviour, such as operating systems.

In algebras with finite and infinite behaviour, some algebraic laws of sequential composition need to be adapted by separating the finite and the infinite traces of a program $x$ into the disjoint sets $\text{fin } x$ and $\text{inf } x$. While the above law $x \cdot 1 = x$ still holds for all elements, the property $x \cdot 0 = 0$ no longer holds when $x$ contains infinite traces; it weakens to $(\text{fin } x) \cdot 0 = 0$. The intuitive explanation is that infinite traces do not terminate, and therefore a possible successor, including **abort**, can never be ‘executed’. Therefore the while-loop now has the more general behaviour

$$ (p \cdot x)^* \cdot \neg p = (p \cdot \text{fin } x)^* \cdot (\neg p + p \cdot \text{inf } x), $$

which means that after a finitely many finite traces from $x$ the loop either terminates by not satisfying the test $p$ any longer, or an infinite trace from $x$ takes over, leading to overall non-termination. When $x$ is purely finite, i.e., satisfies $\text{inf } x = 0$, this reduces to the expression given previously.

Like the operators of semirings, the operators of finite and infinite iterations (and many of their combinations) satisfy a common set of laws, and thus algebra helps to unify their treatment including the derivation of program transformations and refinement theorems. Applications range from termination in classical programs, via protocols, to dynamic and hybrid systems [lxvii].

*Omega algebras* are also used to develop a unified framework for various logics, including the temporal logics LTL, CTL and CTL*, neighbourhood logic and separation logic [lx].

To sum up: algebraic characterisations have helped to express (and prove) new notions and results and to unify concepts and identify the above-mentioned similarities. The Group has developed a coherent view on algorithms and languages from an algebraic perspective, and applies the same algebraic techniques to tackle modern technology, including the analysis of protocols and quantum computing. All the algebras in question provide a first-order equational calculus, which makes them ideal to be supported by *automated theorem provers* and *interactive proof assistants* [lxviii] [xliv]. As a consequence, they are well suited for developing tools that support program derivations and refinement in a (semi-)automated style.

# 8 System support: the right tool for the job

Calculational program construction derives a program from a formal specification by manageable, controlled steps that *because* they are calculated– guarantee that the final product meets its initial specification. As we have seen, this
methodology has been practised by many Group members, and many others
too [lxix]. And it applies to many programming styles, including both functional
and imperative. For the former one uses mostly equational reasoning, applying
the defining equations of functions together with laws of the underlying data
structures. For the latter, inequations deploying a refinement relation are com-
mon [lxx]. A frequent synonym for "calculation rules" is "transformation rules".

A breakthrough occurred when the Group raised the level of reasoning (§2):
from manipulations of imperative code (Abstracto) to algebraic abstractions of
functional control patterns (Squiggol). This made it possible to compact deriva-
tions of several pages in traditional approaches down to one page or even less.
A similar observation concerns the general theme of ‘algebraicisation’ (see §7).

**8.1 System support**

Of course, calculational program construction can be done with pencil and paper,
and initially it should be so: that encourages a simplicity and elegance in its
methods. Ultimately, if the method proves to be useful, there are a number of
good reasons for introducing system support:

- By its very nature, program transformation leads to frequent rewritings of program fragments; such clerical work should be automatic. And, by *its* very nature, a system does this mechanical activity better than a human can.

- The system can record the applicability conditions and help in reducing them to simpler forms, ideally all the way to "true".

- And, as mentioned in §1, the system can construct a *development history*, again a clerical task. This history serves as detailed software documentation, since it reflects every design decision that enters into the final program. Thus, if a line of development turns out to be a blind alley, the history can be used for backtracking to try out alternative design decisions. Moreover, it is the key aid to software maintenance: when the specification has to be modified (because of new requirements), one can try to 'replay' a recorded development accordingly.

Thus the Group gave considerable attention to program transformation sys-
tems [ix] once the methods they automated were sufficiently mature. In the
remainder of this section we take a brief look at one of them: it touches on sev-
eral areas within the Group, and several Group members were involved in it and
in follow-on projects.

**8.2 An example: the project CIP**

The project CIP (*Computer-aided, Intuition-guided Programming*) at TU Mu-
nich ran roughly through the period 1977–1990.
**The wide-spectrum language CIP-L.** The CIP approach was based on a particular 'life cycle of transformational program development', roughly characterised by the following levels [lxxi]:

1. formal problem specification (usually descriptive, not (yet) executable, possibly non-deterministic);

2. recursive functional program;

3. efficiency-improved functional program;

4. deterministic, tail-recursive solution;

5. efficient procedural or machine-oriented program.

However, not all of these levels need occur: a development may start below Level 1 and end above Level 5; and it may skip some of the intermediate levels.

The language CIP-L was however especially designed to cover all five levels [lxxii]. Since transformations usually do not change a program as a whole, only small portions of it, it was mandatory to design one integrated wide-spectrum language rather separate languages for each level. In particular, the language included assertion constructs at all levels, thus allowing the incorporation of pre- and postconditions uniformly for functions and statements — so it is also connected to the refinement calculi that were developed around the same time [lxx]. CIP-L was partly inspired by Abstracto (§2.1); in a sense, it tried to present a model of a possible concrete instance of Abstracto.

**The transformation system CIP-S.** The purpose of CIP-S was the transformational development of programs and program schemes. In addition to bookkeeping tasks, that included the manipulation of concrete programs, the derivation of new transformation rules within the system, and support for the verification of side conditions of transformation rules [lxxiii].

In keeping with the overall CIP methodology, the kernel of the system was itself formally specified: starting from that specification, all routines were developed to Pascal-level CIP-L using an earlier prototype system. The results were embedded into an appropriate user environment, yielding a first operational version of CIP-S around 1990. In conjunction with a compiler for a substantial executable subset of CIP-L, the CIP-S system has been successfully used in education. The transformational approach was continued by the Group.

**Experiences.** There is an extensive body of case studies using the CIP methodology. They concern mostly small and medium-sized algorithms, e.g., sorting and parsing [lxxiv]. The formal development of CIP-S itself showed that the method is suitable for larger software projects too.

## 9 Summary; but no conclusion

This is not a 'conclusion'. And this article is not a history. It is a description of a *goal*, a justification of its importance, and a summary of the trajectory that
has led, and still leads to progress towards that goal. And what we especially enjoy about that trajectory we have followed, right from the start 60 years ago, is that it has always been the same one:

Let us calculate! (§2 p6)

Why is that goal so important?
Writing programs using a careful process of walk-throughs and reviews is (alone) not enough; “growing” programs [lxxv] in a top-down way is (alone) not enough; proving your program correct afterwards is (alone) not enough. We have always believed that maintaining correctness from the very top, and then ‘all the way down’ is what we all should be aiming for.

But will we ever get there? *No, we will not.*

During the 1970’s, an array-out-of-bounds error in a high-level program would typically lead to a core dump, an inch-high stack of paper that was examined at just one spot, an “Ah, yes!” and then the whole thing just thrown away. Thirty years of progress brought us to ‘Interactive Development Environments’ and the internet, where sometimes the programmer was not even sure *where* the just-corrected version of a program had been ‘deployed’, nor exactly *whether* it contained the fix (because of caching). Error messages from a remote server in some far-away city flicked up out of the window, too quickly to be read, and could not be scrolled back. And twenty more years bring us up-to-date, with ‘intelligent’ aquarium thermometers that can be hacked from half a world away and used to raid a company’s private database. *Plus ça change...*

The one constant through all of this is *people*, their tolerance for impediments to getting their work done and their perseverance in spite of them. The technology we are trying to control, to approach rigorously, is always sitting on that boundary, just beyond our reach: we will never calculate far enough.

Thus, however good we become at calculating, and convincing others to do so, there will always be economic forces that promote and propagate computer applications that we *cannot* develop by careful walk-throughs, or grow top-down, or prove correct... or calculate. This ‘catching up’ factor is what drives all the IFIP working groups — we constantly extend our methods improve the impact of computers generally, to make them safer and increase their reliability, as their use becomes ever more ambitious and spreads ever more widely.

We are not so much ‘pushing’ as ‘being pulled’. There is the excitement.

# 10 Detailed attributions and citations

## [i] Contributors —

*All* of the members of WG2.1, past and present, deserve credit for what is reported here. Among those who provided actual text were Richard Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, Johan Jeuring, Lambert Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra and Nicolas Wu.

Carroll Morgan was Group Chair at the time of writing, and is the corresponding author.

## [ii] The founding of IFIP —

It was established on 23 March 1962 [161, 26].

## [iii] Change of name —

At Meeting #39 in Chamrousse in January 1989, Formal Resolution 2 was to recommend to TC2 that the Group’s name be changed to “WG2.1 on ALGOL:”
Algorithmic Languages and Calculi". But TC2 rejected the recommendation, as reported at Meeting #40. At Meeting #41 in Burton in May 1990, it was reported that TC2 suggested instead simply "Algorithmic Languages and Calculi", and this suggestion was accepted by the Group. TC2 approved the change, which was reported at Meeting #42 in Louvain-la-Neuve in January 1991.

[iv] **Assigning meanings to programs** —
This was Floyd's association of predicates with flowchart arcs [71].

[v] **An axiomatic basis for computer programming** —
This was Hoare's logic for partial correctness [96].

[vi] **A Discipline of Programming** —
This was Dijkstra's calculus of weakest preconditions [66].

[vii] **Predicative programming** —
This generalisation was the work of Hoare and Hehner [97, 88, 89].

[viii] **Laws of Programming** —
This work was presented by a number of authors, including Hoare, at Oxford's Programming Research Group [98].

[ix] **Program-transformation systems** —
Systems designed and implemented by Group members include the Argonne TAMPR (Transformation-Assisted Multiple Program Realization) System [43, 42, 41], ARIES (Acquisition of Requirements and Incremental Evolution of Specifications) [114], (R)APTS (Rutgers Abstract Program Transformation System) [165], KIDS (Kestrel Interactive Development System) [188], POPART (Producer of Parsers And Related Tools) [205, 204], ZAP [68, 69], and the Munich CIP (Computer-aided, Intuition-guided Programming) project [21, 23, 151]. Comparisons of various transformation systems are presented in [173, 70].

[x] **The name "Abstracto"** —
The lecturer who made that remark was Leo Geurts [74, p57]; he added that "in abstracto" was Dutch [sic!] for "in the abstract".

[xi] **Criteria for Abstracto** —
These criteria for Abstracto were proposed by Robert Dewar, who was the Group's chairman at the time [65]. His letter was written in July 1977 [65], in advance of Meeting #23 of the Group in Oxford in December of that year. The *New Directions in Algorithmic Languages* conferences were in 1975 and 1976, the work of a subcommittee chaired by Robert Dewar and with proceedings [184, 185] edited by Stephen Schuman.

[xii] **Abstracting Abstracto** —
This landmark step was suggested and developed by Richard Bird and Lambert Meertens.

[xiii] **The Boom Hierarchy** —
The Boom hierarchy was introduced by Hendrik Boom [38], and thus named "Boom" (by others) — another pun, since Hendrik is Dutch, and "boom" is Dutch for tree. Backhouse [11] presents a detailed study of the Boom Hierarchy, and compares it to the quantifier notation introduced by Edsger Dijkstra and colleagues at Eindhoven.

[xiv] **The appeal to category theory** —
The introduction of concepts from category theory was due to Grant Malcolm [127], based on the work of Hagino [87].
[xv] **The connection between type structure and data structure** —

This observation was made by Martin Löf [131], and later by many others, including
by Roland Backhouse in his work on type theory [13].

[xvi] **The Group's diverse interests** —

Our methods have been applied to separation logic [56], pointer structures [144, 34], database queries [148, 80], geographic information systems [147], climate change [111, 109, 39], scientific computation [110], planning [36] and logistics [175], and domain-specific languages for parsing/pretty printing/program calculation.

[xvii] **Beginner's programming languages** —

Beginner's programming languages designed and implemented by Group members include Peter King's *MABEL*, Kees Koster's *ELAN*, and Lambert Meertens' *ABC* [75].

[xviii] **Inspiration for Python** —

ABC's influence on Python [179] can be seen at Guido van Rossum's biographical
page, and at the ABC and Python pages on Wikipedia:

https://gvanrossum.github.io/bio.html

https://en.wikipedia.org/wiki/ABC_(programming_language)

https://en.wikipedia.org/wiki/Python_(programming_language)

[xix] **Revised Report on ALGOL 68** —

ALGOL 68 was designed by WG2.1 at the direction of TC2. On December 20, 1968, the language was formally adopted by the Group, and subsequently approved for publication by the General Assembly of IFIP.

[xx] **Example of Abstracto** —

This example is from Lambert Meertens [137].

[xxi] **Refinement calculus** —

The ‘Abstracto vision’ was Lambert Meertens’. It was developed in much greater depth by Ralph Back (independently) [9, 10] and, later, by Carroll Morgan [153, 155]. When Morgan asked Meertens why he had not pursued the refinement calculus further, Meertens’ reply was “It didn’t work.”

[xxii] **Higher-level reasoning** —

Meertens became disillusioned with Abstracto's low-level transformations, as described in [139]. It was Richard Bird who provided the key insight needed to lift the reasoning to a higher level [30]. Examples are given in [138].

[xxiii] **Program transformations** —

These examples, and many others, were described by Bird [30].

[xxiv] **Evolving notation** —

Bird took the work forwards through the 1980's, notably in a series of tutorial papers [31, 32, 33] produced in quick succession; an example, the calculation for the Maximum Segment Sum problem, is shown in Figure 3.

[xxv] **The names “Squiggol” and “BMF”** —

Meertens recalls that Robert Dewar passed a note to him with the single word "Squigol" on it, making a pun with language names such as ALGOL, COBOL, and SNOBOL [140]. The first appearance of the name in the minutes is for Meeting #35 in Sausalito in December 1985. However, it has come to be written "Squiggol", perhaps to emphasise that the pronunciation should be 'skwiggl' ("qui") rather than 'skwaigbl' ("quae"). Later, at a meeting of the STOP project in Nijmegen in 1988, Doaitse Swierstra coined the more sober name "Bird-Meertens Formalism" (BMF), making a different pun with "Backus-Naur Form" (BNF).
[xxvi] **The Eindhoven quantifier notation —**

The Eindhoven quantifier notation rationalised the notation for binding a variable, determining its range and forming elements from it [11, 156]. In the conventional $\sum_{n=0}^{N} n^2$ for example, the $n$ below the $\Sigma$ is a binding occurrence; but the $n$ in $n^2$ is bound; and the $n^2$ forms elements from that bound variable. The 0 and the $N$ determine the range of $n$, and the $\Sigma$ itself gives the ‘quantifier’, the operation (usually associative and commutative) carried out on the elements. In the Eindhoven notation that would be written in the order quantifier, bound variable(s), range, element-former. The whole expression is *always* enclosed by binding-scope delimiters — so the example above might be written $(+n : 0 \le n \le N : n^2)$. The advantage of using the Eindhoven notation is that uniform calculational laws apply to the manipulation of those expressions, and they greatly reduce the risk of error.

[xxvii] **Catamorphisms —**

Meertens coined the term catamorphism for the unique function induced by a homomorphism from the initial algebra, in a working document presented at Meeting #38 in Rome (1988).

[xxviii] **Datatype-generic programming —**

The term ‘datatype-generic programming’ was coined by Roland Backhouse and Jeremy Gibbons for a project that ran 2003–2006 [14]; the point was to distinguish from the different use of the term ‘generic programming’ in languages like C++, where it essentially means parametric polymorphism. Within the context of the Group, ‘datatype-generic programming’ has come to mean parametrization by a functor, as with catamorphisms, and plain ‘generic programming’ to mean functions defined more specifically over the sum-of-products structure of a polynomial functor, as with PolyP and Generic Haskell.

[xxix] **Polytypic programming languages and PolyP —**

The language PolyP, an extension of the lazy, higher-order functional programming language Haskell [176], was designed by Jansson and Jeuring at Chalmers, Gothenburg [112]. The development of PolyP and its applications was discussed at Meeting #49 in Rancho Santa Fe (1996), Meeting #51 in Oxford (1998), and Meeting #53 in Potsdam (1999).

[xxx] **Generic datatypes with mutual recursion —**

The theory to make Generic Haskell possible was developed by Hinze, a first-time observer in Potsdam (1999). He presented his theory at Meeting #54 in Blackheath (2000) [92]. To support generic functions on sets of mutually recursive datatypes, Hinze, Jeuring, and Löh developed Generic Haskell from 2000 onwards [120, 95]. Various aspects of Generic Haskell were discussed also at Meeting #59 in Nottingham in 2004.

[xxxi] **Type-indexed datatypes —**

Type-indexed datatypes were introduced by Hinze et al. [95]. The type families extension of Haskell is based on the work of Chakravarty et al. [50].

[xxii] **Fixed-point representation of mutually recursive datatypes —**

Rodriguez and others developed MultiRec [181], a generic programming library that uses a fixed-point representation of possibly mutually recursive datatypes.

[xxiii] **Generic programming libraries —**

For an early comparison of generic programming libraries, see Rodriguez et al. [180]. An early variant of Scrap Your Boilerplate [119] was discussed at Meeting #56 on
Ameland, The Netherlands (2001). Generic Deriving [123] was discussed at Meeting #70 in Ulm.

[xxxiv] **Catamorphisms** —
This work was done mainly by Grant Malcolm [127].

[xxxv] **A zoo of morphisms** —
There were mutumorphisms [72], which are pairs of mutually recursive functions; zygomorphisms [126], which consist of a main recursive function and an auxiliary one on which it depends; histomorphisms [198], in which the body has access to the recursive images of all subterms, not just the immediate ones; so-called generalised folds [28], which use polymorphic recursion to handle nested datatypes; and then there were generic accumulations [166], which keep intermediate results in additional paramters for later stages in the computation.

[xxxvi] **Paramorphism** —
This was introduced by Lambert Meertens at Meeting #41 in Burton, UK (1990) [141].

[xxxvii] **Recursion schemes from comonads** —
This appeared in Uustalu et al [200]. Comonads capture the general idea of ‘evaluation in context’ [199], and this scheme makes contextual information available to the body of the recursion. It was used to subsume both zygomorphisms and histomorphisms.

[xxxviii] **Adjoint folds** —
This was done by Hinze [93]. Using adjunctions as the common thread, adjoint folds arise by inserting a left adjoint functor into the recursive characterisation, thereby adapting the form of the recursion; they subsume paramorphisms, accumulating folds, mutumorphisms (and hence zygomorphisms), and generalised folds. Later, it was observed that adjoint folds could be used to subsume recursion schemes from comonads by Hinze and Wu [94].

[xxxix] **Constructive mathematics and computer programming** —
The connection between constructive mathematics and computer programming was pioneered by the Swedish philosopher and logician Per Martin-Löf [132].

[xl] **Programming languages implementing dependent types** —
Programming languages with dependent types include ALF [125], Cayenne [7], ATS [206], Epigram [134], Agda [162] and Idris [44].

[xli] **Curry-Howard correspondence** —
The Curry-Howard correspondence describes how the typing rules of the lambda calculus are in one-to-one correspondence with the natural deduction rules in logic. Wadler [203] gives a historic overview of this idea, aimed at a more general audience.

[xlii] **Generic programming in dependently typed languages** —
The idea of using dependent types to define an explicit *universe* of types was one of the early applications of dependently typed programming [4, 27]. Since then, there have been several PhD theses exploring this idea further [53, 116, 158, 124, 162, 57]

[xliii] **WG2.1 and dependent types** —
Backhouse started exploring type theory in the mid 1980's [13]. At Meeting #42, Nordström was invited as an observer and talked about the work on ALF. Throughout the early 21st century, observers and members were frequently active in the
area of type theory or generic programming, including McBride, Löh, Jansson, Swierstra, Dagand, McKinna and many others.

[xliv] **Algebra of programming in Agda** —
Patrik Jansson gave a first tutorial on the dependently typed programming lan-
guage Agda at Meeting #63 in Kyoto in 2007. This lead to an exploration of how
to mechanize the kind of program that was previously carried out on paper [159].

[xlv] **Program calculation and type theory** —
As type theory is a language for describing both proofs and programs, it is no
surprise that it provides the ideal setting for formalizing the program calculation
techniques that members of the Group pioneered [3, 193, 195].

[xlvi] **Applications of dependent types** —
As languages with dependent types matured, various researchers started exploring
novel and unexpected applications in a variety of domains [110, 40, 111, 58].

[xlvii] **Dependently typed combinator parsing** —
This was for example investigated by Nils Danielsson [59].

[xlviii] **Dependent types and program development** —
Many modern dependently typed programming languages are equipped with some
sort of IDE. Once the type signature of a method has been fixed, the programmer
can interactively find a suitable definition. There are numerous examples of how a
powerful type signature can give strong guarantees about a data structure’s invari-
ants [133], the correctness of a domain-specific language [60], or type preservation
of a compiler [136].

[xlix] **Dependent types and effects** —
There is a large body of work studying how to incorporate side-effects in depen-
dently typed programming languages. This can be done by constructing deno-
tational models [192, 194], by adding new effectful primitives to the type the-
ory [160], or by giving an algebraic account of the properties that laws that effects
satisfy [45, 78].

[l] **Monads** —
This insight was made by Eugenio Moggi while studying semantics of programming
languages [143].

[li] **Kleisli arrows** —
Mike Spivey adopted this notion of monads for writing purely functional programs
with exceptions [189]; Phil Wadler generalized it to other effects, and popularized
it as the main abstraction for dealing with effects in Haskell [201, 202].

[lii] **Parser combinators** —
The combinator style of parsing is due to William Burge [48]. The monadic pre-
sentation was popularized by Graham Hutton and Erik Meijer [108], and a depen-
dently typed version presented by Nils Danielsson [xlvii].

[liii] **Parsers in verse** —
The verse characterization of the parser type is due Fritz Ruehr [182].

[liv] **Applicative functors** —
The applicative interface for parsers was invented by Doaitse Swierstra [191]. This
and other applications inspired Conor McBride and Ross Paterson to identify the
abstraction of *applicative functors* (also called "strong lax-monoidal functors" or
"idioms") [135]. Like monads, applicative functors have turned out to have unfore-
seen applications, such as in datatype traversals [79, 29] and distributed computing
[76].

[lv] Algebraic effects —

Purely functional specifications of effects were studied by Wouter Swierstra in his PhD thesis [192, 194]. The axioms of an algebraic specification can be applied to equational reasoning involving either combinators or the imperative-flavoured comprehension notation provided for example by Haskell's **do** notation [78]. Algebraic effects and handlers were introduced by Gordon Plotkin then explored more fully in Matija Pretnar's PhD thesis [178], and are now the subject of much active work in the Group and beyond.

[lvi] Applications of relation algebra —

Roland Backhouse and B.A. Carré discovered similarities between an algebra for path problems and the algebra of regular languages [15]. Tony Hoare and others developed algebraic laws of programming, insisting that "specifications obey all the laws of the calculus of relations" [98]. Richard Bird and Oege de Moor used relations for the calculational derivation of programs covering principles of algorithm design such as dynamic programming, greedy algorithms, exhaustive search and divide and conquer [35].

[lvii] Algebra of binary relations —

Calculi based on the algebra of binary relations were developed by George Boole, Charles Peirce, Ernst Schröder, Augustus De Morgan and Alfred Tarski [174, 183, 197]

[lviii] Graph algorithms —

Walter Guttmann, for example, showed that the same correctness proof shows that well-known algorithms solve the minimum weight spanning tree problem, the minimum bottleneck spanning tree problem and similar optimisation problems with different aggregation functions [85]. Algebraic versions of Dijkstra's shortest path algorithm and the one by Floyd/Warshall are applications of these algorithms to structures different from graphs, pinpointing the mathematical requirements on the underlying cost algebra that ensure their correctness [103]. Roland Backhouse and colleagues are currently writing a book on algorithmic graph theory presented relationally [18].

[lx] Program analysis —

Program analysis using an algebraic style of reasoning has always been a core activity of the Group; for examples see [67, 64, 63].

[lx] Pointer structures —

Bernhard Möller and Richard Bird researched representations of data structures in general, and pointer structures in particular [144, 34].

[lxi] Algebraic logics —

An important step to an algebraic form of program logic was taken by Hoare and his colleagues [98]. More recently, the central aspects of Separation Logic [164, 163] were treated algebraically [56, 54, 55].

Next to programming semantics, the infinite iteration operator can be applied to model various logics. The temporal logics LTL, CTL and CTL* have been in [115, 152, 61]. There were studies on logics for hybrid systems [101, 102] and Neighbourhood Logic [100].
[lxii] **Further applications of the algebraic approach —**

The Group discovered countless areas in computer science where semirings are the underlying structure. Applications reach from, fundamental concepts of programming language semantics, including concurrent programs [99] and termination [91, 67, 62, 16] via games [186, 12, 17] and data processing [177], to multi-agent systems [146] and quantum computing [196].

Beyond that, matrix-style reasoning has applications in object-oriented programming [122] and feature-oriented software development, including aspects of product families [107] and of feature interactions [20].

[lxiii] **Algebraic semantics of the while loop —**

The fixed-point characterisation of while loops goes back to Andrzej Blikle and David Park [37, 167]. Dexter Kozen transferred the concept into the setting of Kleene algebras [117].

[lxiv] **Algebras with tests —**

Test elements form a Boolean subalgebra. It represents an algebraic version of the usual assertion logics like the Hoare calculus [118, 149]. There is a direct link to weakest (liberal) preconditions [35, 150].

[lxv] **Fixed-point fusion —**

Fixed-point fusion is a consequence of the fixed-point semantics of recursion [142, 1].

[lxvi] **Virtual data structures —**

These were described by Doaitse Swierstra and Oege de Moor [190].

[lxvii] **Omega algebras —**

The omega operator was introduced by Cohen [51]; Möller performed a systematic study of its foundations [145].

Guttmann used it for analysing executions of lazy and strict computations [83]. Infinite traces, also called *streams*, have many applications including the modelling protocols [144], as well as dynamic and hybrid systems [186, 187, 101]. The corresponding algebras can also be used to formally reason about (non)termination in classical programs [105].

[lxviii] **Tool-Support for algebraic reasoning —**

Peter Höfner and Georg Struth proved countless theorems of all these algebras in automated theorem provers, such as Prover9 [104, 106]. Walter Guttmann, Peter Höfner, Georg Struth and others used the interactive proof assistant Isabelle/HOL to implement the algebras, the concrete models, as well as many program derivations, e.g. [5, 81, 6, 84].

[lxix] **Program transformation —**

In the functional realm, fundamental ideas in program transformation were introduced by Cooper [52] and subsequently developed by others, in particular Burstall and Darlington [49]. Later activities occurred within the ISI project [19, 121] and at Kestrel Institute [82]. In the realm of artificial intelligence there were ideas in the field of automated programming (e.g., the DEDALUS system [128] and its successor [129, 130]).

[xx] **Refinement calculi —**

Imperative programming calculi based on refinement include those of Dijkstra [66], Back [8], Hoare [97, 98], Hehner [88, 89, 90], Morris [157], and Morgan [154, 155].
[lxxi] **Transformational development** —

For background on the 'life cycle of transformational program development', see Broy [2]. The five levels of the 'wide spectrum' are due to Partsch [171].

[lxxii] **The language CIP-L** —

The language CIP-L is described in detail in the first of two volumes about the CIP project as a whole [24]. For some of the motivation, see Bauer [22] and Broy and Pepper [47].

[lxxiii] **The system CIP-S** —

The specification of the CIP-S system can be found in the second volume about the CIP project [25]. The more interesting parts of the formal development of the system, together with the transformation rules used, can also be found there. Successors to CIP-S were developed by Partsch [172] and Guttmann et al. [86].

[lxxiv] **Experiences with CIP** —

Smaller CIP case studies include sorting [46, 168] and parsing [170, 169, 171]. As noted above, the CIP-S system itself [25] constitutes a larger case study.

[lxxv] **Programs should be grown** —

Fred Brooks wrote "Some years ago Harlan Mills proposed that any software system should be grown by incremental development." [73]

**Acknowledgements**

§2 is based on a paper more specifically about the evolution of the Bird-Meertens Formalism [77], §3 partly based on a paper about the contributions to generic programming of the Software Technology group at Utrecht University [113], and §4 partly based on a paper about the unification of recursion schemes [94].
Bibliography

[1] Aarts C, Backhouse R, Boiten E, Doornbos H, van Gasteren N, van Gel-
drop R, Hoogendijk P, Voermans E, van der Woude J (1995) Fixed-point
calculus. Information Processing Letters 53(3):131–136

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

[3] Alpuim J, Swierstra W (2018) Embedding the refinement calculus in Coq.
Science of Computer Programming 164:37–48

[4] Altenkirch T, McBride C (2003) Generic programming within dependently
typed programming. In: Gibbons J, Jeuring J (eds) Generic Programming,
Springer, pp 1–20

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

[6] Armstrong A, Foster S, Struth G, Weber T (2014) Relation alge-
bra. Archive of Formal Proofs http://isa-afp.org/entries/Relation_
Algebra.html

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

[8] Back RJ (1978) On the correctness of refinement steps in program devel-
opment. PhD thesis. Report A-1978-4, Department of Computer Science,
University of Helsinki

[9] Back RJ (1981) On correct refinement of programs. Journal of Computer
and System Sciences 23(1):49–68, DOI 10.1016/0022-0000(81)90005-2

[10] Back RJ, von Wright J (1998) Refinement Calculus: A Systematic Intro-
duction. Graduate Texts in Computer Science, Springer

[11] Backhouse R (1988) An exploration of the Bird-Meertens formalism. Tech.
Rep. CS 8810, Department of Computer Science, Groningen University

[12] Backhouse R, Michaelis D (2004) 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, Springer, Lecture Notes in Computer Science, vol 3051, pp 34–47

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

[14] Backhouse R, Gibbons J, Hinze R, Jeuring J (eds) (2007) Spring School on Datatype-Generic Programming, Lecture Notes in Computer Science, vol 4719, Springer-Verlag, DOI 10.1007/978-3-540-76786-2

[15] Backhouse RC, Carré BA (1975) Regular algebra applied to path-finding problems. IMA Journal of Applied Mathematics 15(2):161–186, DOI 10.1093/imamat/15.2.161

[16] Backhouse RC, Doornbos H (2008) Datatype-generic termination
proofs. Theory of Computing Systems 43(3-4):362–393, DOI 10.1007/
s00224-007-9056-z
[17] Backhouse RC, Chen W, Ferreira JF (2013) The algorithmics of solitaire-like games. Science of Computer Programming 78(11):2029-2046, DOI 10.1016/j.scico.2012.07.007

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

[19] Balzer R, Goldman N, Wile D (1976) On the transformational implementation approach to programming. In: Yeh RT, Ramamoorthy CV (eds) International Conference on Software Engineering, IEEE Computer Society, pp 337-344

[20] Batory DS, Höfner P, Kim J (2011) Feature interactions, products, and composition. In: Denney E, Schultz UP (eds) Generative Programming and Component Engineering, ACM, pp 13-22, DOI 10.1145/2047862.2047867

[21] Bauer FL (1976) Programming as an evolutionary process. In: Yeh RT, Ramamoorthy C (eds) International Conference on Software Engineering, IEEE Computer Society, pp 223-234

[22] Bauer FL (1982) From specifications to machine code: Program construction through formal reasoning. In: Ohno Y, Basili V, Enomoto H, Kobayashi K, Yeh RT (eds) International Conference on Software Engineering, IEEE Computer Society, pp 84-91

[23] Bauer FL, Wössner H (1982) Algorithmic Language and Program Development. Texts and Monographs in Computer Science, Springer, DOI 10.1007/978-3-642-61807-9

[24] Bauer FL, Berghammer R, Broy M, Dosch W, Geiselbrechtinger F, Gnatz R, Hangel E, Hesse W, Krieg-Brückner B, Laut A, Matzner T, Möller B, Nickl F, Partsch H, Pepper P, Samelson K, Wirsing M, Wössner H (1985) The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L, Lecture Notes in Computer Science, vol 183. Springer, DOI 10.1007/3-540-15187-7

[25] Bauer FL, Ehler H, Horsch A, Möller B, Partsch H, Paukner O, Pepper P (1987) The Munich Project CIP, Volume II: The Program Transformation System CIP-S, Lecture Notes in Computer Science, vol 292. Springer-Verlag, Berlin

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

[27] Benke M, Dybjer P, Jansson P (2003) Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing 10(4):265-289

[28] Bird R, Paterson R (1999) Generalised folds for nested datatypes. Formal Aspects of Computing 11(2):200-222, DOI 10.1007/s001650050047

[29] Bird R, Gibbons J, Mehner S, Voigtländer J, Schrijvers T (2013) Understanding idiomatic traversals backwards and forwards. In: Haskell Symposium, ACM, DOI 10.1145/2503778.2503781

[30] Bird RS (1981) 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
[31] Bird RS (1986) An introduction to the theory of lists. Monograph PRG-56, Programming Research Group, University of Oxford

[32] Bird RS (1987) A calculus of functions for program derivation. Monograph PRG-64, Programming Research Group, University of Oxford

[33] Bird RS (1988) Lectures on constructive functional programming. Monograph PRG-69, Programming Research Group, University of Oxford

[34] Bird RS (2001) Unfolding pointer algorithms. Journal of Functional Programming 11(3):347–358, DOI 10.1017/S0956796801003914

[35] Bird RS, de Moor O (1997) Algebra of Programming. Prentice Hall International Series in Computer Science, Prentice Hall

[36] Blaine L, Gilham L, Liu J, Smith DR, Westfold SJ (1998) Planware: Domain-specific synthesis of high-performance schedulers. In: Automated Software Engineering, IEEE Computer Society, p 270, DOI 10.1109/ASE. 1998.732672

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

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

[39] Botta N, Jansson P, Ionescu C (2017) Contributions to a computational theory of policy advice and avoidability. Journal of Functional Programming 27:e23, DOI 10.1017/S0956796817000156

[40] Botta N, Jansson P, Ionescu C, Christiansen DR, Brady E (2017) Sequential decision problems, dependent types and generic solutions. Logical Methods in Computer Science 13(1), DOI 10.23638/LMCS-13(1:7)2017

[41] Boyle J, Harmer TJ, Winter VL (1996) The TAMPR program transformation system: Simplifying the development of numerical software. In: Arge E, Bruaset AM, Langtangen HP (eds) Modern Software Tools for Scientific Computing, Birkhäuser, pp 353–372, DOI 10.1007/978-1-4612-1986-6_17

[42] Boyle JM (1976) An introduction to Transformation-Assisted Multiple Program Realization (tampr) system. In: Bunch JR (ed) Cooperative Development of Mathematical Software, Dept.of Mathematics, University of California, San Diego

[43] Boyle JM, Dritz KW (1974) An automated programming system to facilitate the development of quality mathematical software. In: Rosenfeld J (ed) IFIP Congress, North-Holland, pp 542–546

[44] Brady E (2013) Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23(5):552–593

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

[46] Broy M (1983) Program construction by transformations: A family tree of sorting programs. In: Biermann A, Guiho G (eds) Computer Program Synthesis Methodologies, Springer, NATO Advanced Study Institutes Series, vol 95
[47] Broy M, Pepper P (1983) 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

[48] Burge WH (1975) Recursive Programming Techniques. Addison-Wesley

[49] Burstall RM, Darlington J (1977) A transformation system for developing recursive programs. Journal of the ACM 24(1):44–67

[50] Chakravarty MMT, Keller G, Peyton Jones SL, Marlow S (2005) Associated types with class. In: Palsberg J, Abadi M (eds) Principles of Programming Languages, ACM, pp 1–13, DOI 10.1145/1040305.1040306

[51] Cohen E (2000) Separation and reduction. In: Backhouse R, Oliveira JN (eds) Mathematics of Program Construction, Springer, Lecture Notes in Computer Science, vol 1837, pp 45–59

[52] Cooper D (1966) The equivalence of certain computations. Computing Journal 9:45–52

[53] Dagand PE, et al (2013) A cosmology of datatypes: Reusability and dependent types. PhD thesis, University of Strathclyde

[54] Dang H, Möller B (2013) Concurrency and local reasoning under reverse exchange. Science of Computer Programming 85, Part B:204–223

[55] Dang H, Möller B (2015) Extended transitive separation logic. Journal of Logical and Algebraic Methods in Programming 84(3):303–325, DOI 10.1016/j.jlamp.2014.12.002

[56] Dang H, Höfner P, Möller B (2011) Algebraic separation logic. Journal of Logic and Algebraic Programming 80(6):221–247, DOI 10.1016/j.jlap.2011.04.003

[57] Danielsson NA (2007) Functional program correctness through types. PhD thesis, Chalmers University of Technology and Gothenburg University

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

[59] Danielsson NA (2010) Total parser combinators. In: International Conference on Functional Programming, pp 285–296

[60] Danielsson NA (2013) Correct-by-construction pretty-printing. In: Workshop on Dependently-Typed Programming, pp 1–12

[61] Desharnais J, Möller B (2017) 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, DOI 10.1007/978-3-319-57418-9_6

[62] Desharnais J, Möller B, Struth G (2004) Termination in modal Kleene algebra. In: Lévy JJ, Mayr EW, Mitchell JC (eds) Exploring New Frontiers of Theoretical Informatics, Kluwer, pp 647–660

[63] Desharnais J, Möller B, Struth G (2006) Kleene algebra with domain. ACM Transactions on Computational Logic 7(4):798–833

[64] Desharnais J, Möller B, Tchier F (2006) Kleene under a modal demonic star. Journal of Logic and Algebraic Programming 66(2):127–160, DOI 10.1016/j.jlap.2005.04.006

[65] Dewar R (1977) Letter to members of IFIP WG2.1, http://ershov-arc.iis.nsk.su/archive/eaindex.asp?did=29067
[66] Dijkstra EW (1976) A Discipline of Programming. Prentice Hall

[67] Doornbos H, Backhouse RC (2000) Algebra of program termination. In: Backhouse RC, Crole RL, Gibbons J (eds) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Springer, Lecture Notes in Computer Science, vol 2297, pp 203–236, DOI 10.1007/3-540-47797-7_6

[68] Feather MS (1979) A system for developing programs by transformation. PhD thesis, University of Edinburgh, UK, URL http://hdl.handle.net/1842/7296

[69] Feather MS (1982) A system for assisting program transformation. ACM Transactions on Programming Languages 4(1):1–20, DOI 10.1145/357153.357154

[70] Feather MS (1987) A survey and classification of some program transformation approaches and techniques. In: Meertens L (ed) Program Specification and Transformation, North-Holland, pp 165–195

[71] Floyd RW (1967) Assigning meaning to programs. In: Schwartz JT (ed) Mathematical Aspects of Computer Science, American Mathematical Society, Proceedings of Symposia in Applied Mathematics, vol 19, pp 19–32

[72] Fokkinga M (1990) Tupling and mutumorphisms. The Squigglist 1(4):81–82

[73] Fred Brooks J (1975) The Mythical Man-Month. Addison-Wesley

[74] Geurts L, Meertens L (1978) Remarks on Abstracto. Algol Bulletin 42:56–63

[75] Geurts L, Meertens L, Pemberton S (1990) The ABC Programmer's Handbook. Prentice-Hall, iSBN 0-13-000027-2

[76] Gibbons J (2016) Free delivery (functional pearl). In: Haskell Symposium, pp 45–50, DOI 10.1145/2976002.2976005

[77] Gibbons J (2020) 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, to appear

[78] Gibbons J, Hinze R (2011) Just do it: Simple monadic equational reasoning. In: International Conference on Functional Programming, pp 2–14, DOI 10.1145/2034773.2034777

[79] Gibbons J, dos Santos Oliveira BC (2009) The essence of the Iterator pattern. Journal of Functional Programming 19(3,4):377–402, DOI 10.1017/S0956796809007291

[80] Gibbons J, Henglein F, Hinze R, Wu N (2018) Relational algebra by way of adjunctions. Proceedings of the ACM on Programming Languages 2(ICFP):86:1–86:28, DOI 10.1145/3236781

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

[82] Green C, Philipps J, Westfold S, Pressburger T, Kedzierski B, Angebranndt S, Mont-Reynaud B, Tappel S (1981, revised 1982) Research on knowledge-based programming and algorithm design. Tech. Rep. Kes.U.81.2, Kestrel Institute
[83] Guttmann W (2015) Infinite executions of lazy and strict computations. Journal of Logical and Algebraic Methods in Programming 84(3):326–340, DOI 10.1016/j.jlamp.2014.08.001

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

[85] Guttmann W (2018) An algebraic framework for minimum spanning tree problems. Theoretical Computer Science 744:37–55

[86] Guttmann W, Partsch H, Schulte W, Vullinghs T (2003) Tool support for the interactive derivation of formally correct functional programs. Journal of Universal Computer Science 9(2):173, DOI 10.3217/jucs-009-02-0173

[87] Hagino T (1987) A categorical programming language. PhD thesis, University of Edinburgh, UK

[88] Hehner ECR (1984) Predicative programming, part I. Communications of the ACM 27(2):134–143, DOI 10.1145/69610.357988

[89] Hehner ECR (1984) Predicative programming, part II. Communications of the ACM 27(2):144–151, DOI 10.1145/69610.357990

[90] Hehner ECR (1993) A practical theory of programming. Springer

[91] Hehner ECR (1999) Specifications, programs, and total correctness. Science of Computer Programming 34(3):191–205, DOI 10.1016/S0167-6423(98)00027-6

[92] Hinze R (2002) Polytypic values possess polykinded types. Science of Computer Programming 43(2-3):129–159

[93] Hinze R (2013) Adjoint folds and unfolds—an extended study. Science of Computer Programming 78(11):2108–2159, DOI 10.1016/j.scico.2012.07.011

[94] Hinze R, Wu N (2016) Unifying structured recursion schemes: An extended study. Journal of Functional Programming 26:47

[95] Hinze R, Jeuring J, Löh A (2004) Type-indexed data types. Science of Computer Programming 51(1-2):117–151

[96] Hoare CAR (1969) An axiomatic basis for computer programming. Communications of the ACM 12(10):576–580, DOI 10.1145/363235.363259

[97] Hoare CAR (1984) Programs are predicates. Philosophical Transactions of the Royal Society of London (A 312):475–489

[98] Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Communications of the ACM 30(8):672–686, DOI 10.1145/27651.27653

[99] Hoare T, Möller B, Struth G, Wehrman I (2011) Concurrent Kleene algebra and its foundations. Journal of Logic and Algebraic Programming 80(6):266–296, DOI 10.1016/j.jlap.2011.04.005

[100] Höfner P, Möller B (2008) Algebraic neighbourhood logic. Journal of Logic and Algebraic Programming 76:35–59

[101] Höfner P, Möller B (2009) An algebra of hybrid systems. Journal of Logic and Algebraic Programming 78:74–97, DOI 10.1016/j.jlap.2008.08.005

[102] Höfner P, Möller B (2011) Fixing Zeno gaps. Theoretical Computer Science 412(28):3303–3322, DOI 10.1016/j.tcs.2011.03.018
[103] Höfner P, Möller B (2012) Dijkstra, Floyd and Warshall meet Kleene. Formal Aspects of Computing 24(4-6):459-476, DOI 10.1007/s00165-012-0245-4

[104] Höfner P, Struth G (2007) Automated reasoning in Kleene algebra. In: Pfennig F (ed) Automated Deduction, Springer, Lecture Notes in Computer Science, vol 4603, pp 279-294

[105] Höfner P, Struth G (2008) Non-termination in idempotent semirings. In: Berghammer R, Möller B, Struth G (eds) Relations and Kleene Algebra in Computer Science, Springer, Lecture Notes in Computer Science, vol 4988, pp 206-220

[106] Höfner P, Struth G (2008) On automating the calculus of relations. In: Armando A, Baumgartner P, Dowek G (eds) International Joint Conference on Automated Reasoning, Springer, Lecture Notes in Computer Science, vol 5159, pp 50-66

[107] Höfner P, Khédri R, Möller B (2011) Supplementing product families with behaviour. Software and Informatics 5(1-2):245-266

[108] Hutton G, Meijer E (1998) Monadic parsing in haskell. Journal of Functional Programming 8(4):437-444, DOI 10.1017/S0956796898003050

[109] Ionescu C (2016) Vulnerability modelling with functional programming and dependent types. Mathematical Structures in Computer Science 26(1):114-128, DOI 10.1017/S0960129514000139

[110] Ionescu C, Jansson P (2012) Dependently-typed programming in scientific computing. In: Symposium on Implementation and Application of Functional Languages, Springer, pp 140-156

[111] Ionescu C, Jansson P (2013) Testing versus proving in climate impact research. In: TYPES 2011, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, Leibniz International Proceedings in Informationics (LIPIcs), vol 19, pp 41-54, DOI 10.4230/LIPIcs.TYPES.2011.41

[112] Jansson P, Jeuring J (1997) PolyP — a polytypic programming language extension. In: Principles of Programming Languages, pp 470-482

[113] Jeuring J, Meertens L (2009) 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

[114] Johnson WL, Feather MS, Harris DR (1991) The KBSA requirements/specifications facet: ARIES. In: Knowledge-Based Software Engineering, IEEE Computer Society, pp 48-56, DOI 10.1109/KBSE.1991.638020

[115] von Karger B, Berghammer R (1998) A relational model for temporal logic. Logic Journal of the IGPL 6:157-173

[116] Ko HS (2014) Analysis and synthesis of inductive families. DPhil thesis, Oxford University, UK

[117] Kozen D (1997) Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3):427-443

[118] Kozen D (2000) On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic 1(1):60-76
[119] Lämmel R, Peyton Jones S (2003) Scrap your boilerplate: A practical design pattern for generic programming. In: Types in Language Design and Implementation, pp 26–37

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

[121] London P, Feather M (1982) Implementing specification freedoms. Science of Computer Programming 2(2):91–131

[122] Macedo H, Oliveira JN (2015) A linear algebra approach to OLAP. Formal Aspects Computing 27(2):283–307, DOI 10.1007/s00165-014-0316-9

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

[124] Magalhães JPR (2012) Less is more: Generic programming theory and practice. PhD thesis, Utrecht University, Netherlands

[125] Magnusson L, Nordström B (1993) The ALF proof editor and its proof engine. In: International Workshop on Types for Proofs and Programs, Springer, pp 213–237

[126] Malcolm G (1990) Algebraic data types and program transformation. PhD thesis, University of Groningen

[127] Malcolm G (1990) Data structures and program transformation. Science of Computer Programming 14:255–279

[128] Manna Z, Waldinger RJ (1979) Synthesis: Dreams → programs. IEEE Transactions on Software Engineering 5(4):294–328, DOI 10.1109/TSE. 1979.234198

[129] Manna Z, Waldinger RJ (1980) A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems 2(1):90–121, DOI 10.1145/357084.357090

[130] Manna Z, Waldinger RJ (1993) The Deductive Foundations of Computer Programming. Addison-Wesley

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

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

[133] McBride C (2014) How to keep your neighbours in order. In: International Conference on Functional Programming, Association for Computing Machinery, New York, NY, USA, ICFP '14, pp 297–309, DOI 10.1145/2628136.2628163

[134] McBride C, McKinna J (2004) The view from the left. Journal of Functional Programming 14(1):69–111

[135] McBride C, Paterson R (2008) Applicative programming with effects. Journal of Functional Programming 18(1):1–13, DOI 10.1017/S0956796807006326

[136] McKinna J, Wright J (2006) A type-correct, stack-safe, provably correct, expression compiler in Epigram, unpublished draft
[137] Meertens L (1979) Abstracto 84: The next generation. In: Proceedings of the 1979 Annual Conference, ACM, pp 33–39

[138] Meertens L (1986) Algorithmics: Towards programming as a mathematical activity. In: de Bakker JW, Hazewinkel M, Lenstra JK (eds) Proceedings of the CWI Symposium on Mathematics and Computer Science, North-Holland, pp 289–334, available at https://ir.cwi.nl/pub/20634

[139] Meertens L (1987) An Abstracto reader prepared for IFIP WG 2.1. Tech. Rep. CS-N8702, CWI, Amsterdam

[140] Meertens L (2019) Squiggol versus Squigol, private email to JG

[141] Meertens LGLT (1992) Paramorphisms. Formal Aspects of Computing 4(5):413–424

[142] Meijer E, Fokkinga MM, Paterson R (1991) Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes J (ed) Functional Programming Languages and Computer Architecture, Springer, Lecture Notes in Computer Science, vol 523, pp 124–144, DOI 10.1007/3540543961-7

[143] Moggi E (1991) Notions of computation and monads. Information and Computation 93(1)

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

[145] Möller B (2007) Kleene getting lazy. Science of Computer Programming 65:195–214

[146] Möller B (2013) Modal knowledge and game semirings. The Computer Journal 56(1):53–69, DOI 10.1093/comjnl/bxs140

[147] Möller B (2019) Geographic wayfinders and space-time algebra. Journal of Logical and Algebraic Methods in Programming 104:274–302, DOI 10.1016/j.jlamp.2019.02.003

[148] Möller B, Roocks P (2015) An algebra of database preferences. Journal of Logical and Algebraic Methods in Programming 84(3):456–481, DOI 10.1016/j.jlamp.2015.01.001

[149] Möller B, Struth G (2004) Modal Kleene algebra and partial correctness. In: Rattray C, Maharaj S, Shankland C (eds) Algebraic Methodology and Software Technology, Springer, Lecture Notes in Computer Science, vol 3116, pp 379–393, DOI 10.1007/978-3-540-27815-3_30

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

[151] Möller B, Partsch H, Pepper P (1983) Programming with transformations: An overview of the Munich CIP project

[152] Möller B, Höfner P, Struth G (2006) Quantales and temporal logics. In: Johnson M, Vene V (eds) Algebraic Methodology and Software Technology, Springer, Lecture Notes in Computer Science, vol 4019, pp 263–277

[153] Morgan C (1988) The specification statement. ACM Transactions on Programming Languages and Systems 10(3):403–419, DOI 10.1145/44501.44503
[154] Morgan C (1988) The specification statement. ACM Trans Program Lang Syst 10(3):403–19

[155] Morgan C (1990) Programming from Specifications. Prentice Hall

[156] Morgan C (2014) An old new notation for elementary probability theory. Science of Computer Programming 85:115–136, DOI https://doi.org/10.1016/j.scico.2013.09.003, special Issue on Mathematics of Program Construction 2012

[157] Morris JM (1987) A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming 9(3):287–306

[158] Morris PW (2007) Constructing universes for generic programming. PhD thesis, University of Nottingham, UK

[159] Mu SC, Ko HS, Jansson P (2009) Algebra of programming in Agda: Dependent types for relational program derivation. Journal of Functional Programming 19(5):545–579

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

[161] Naur P (1962) The IFIP Working Group on ALGOL. ALGOL Bulletin (Issue 15):52

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

[163] O'Hearn P (2007) Resources, concurrency, and local reasoning. Theoretical Computer Science 375:271–307

[164] O'Hearn PW, Reynolds JC, Yang H (2001) Local reasoning about programs that alter data structures. In: Fribourg L (ed) Computer Science Logic, Springer, Lecture Notes in Computer Science, vol 2142, pp 1–19

[165] Paige R (1983) Transformational programming — Applications to algorithms and systems. In: Wright JR, Landweber L, Demers AJ, Teitelbaum T (eds) Principles of Programming Languages, ACM, pp 73–87, DOI 10.1145/567067.567076

[166] Pardo A (2002) 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

[167] Park D (1979) On the semantics of fair parallelism. In: Bjorner D (ed) Abstract Software Specifications, 1979 Copenhagen Winter School, Springer, Lecture Notes in Computer Science, vol 86, pp 504–526, DOI 10.1007/3-540-10007-5_47

[168] Partsch H (1983) An exercise in the transformational derivation of an efficient program by joining development of control and data structure. Science of Computer Programming 3(1):1–35, DOI 10.1016/0167-6423(83)90002-3

[169] Partsch H (1984) Structuring transformational developments: A case study based on earley's recognizer. Science of Computer Programming 4(1):17–44, DOI 10.1016/0167-6423(84)90010-8

[170] Partsch H (1984) Transformational derivation of parsing algorithms executable on parallel architectures. In: Ammann U (ed) Programmier-
sprachen und Programmentwicklung, Springer, Informatik-Fachberichte,
vol 77, pp 41–57, DOI 10.1007/978-3-642-69393-9_3

[171] Partsch H (1986) Transformational program development in a particular program domain. Science of Computer Programming 7(2):99-241, DOI 10.1016/0167-6423(86)90008-0

[172] Partsch H (1990) Specification and Transformation of Programs — A Formal Approach to Software Development. Texts and Monographs in Computer Science, Springer, DOI 10.1007/978-3-642-61512-2

[173] Partsch H, Steinbrüggen R (1983) Program transformation systems. ACM Computing Surveys 15(3):199-236

[174] Peirce CS (1870) Description of a notation for the logic of relatives, resulting from an amplification of the conceptions of Boole's calculus of logic. Memoirs of the American Academy of Arts and Sciences 9:317-378

[175] Pepper P, Smith DR (1997) A high-level derivation of global search algorithms (with constraint propagation). Science of Computer Programming 28(2-3):247-271, DOI 10.1016/S0167-6423(96)00023-8

[176] Peyton Jones S, et al (2003) Haskell 98, Language and Libraries. The Revised Report. Cambridge University Press, a special issue of the Journal of Functional Programming

[177] Pontes R, Matos M, Oliveira J, Pereira JO (2015) Implementing a linear algebra approach to data processing. In: Cunha J, Fernandes JP, Lämmel R, Saraiva J, Zaytsev V (eds) Grand Timely Topics in Software Engineering, Springer, Lecture Notes in Computer Science, vol 10223, pp 215-222, DOI 10.1007/978-3-319-60074-1_9

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

[179] Python Software Foundation (1997) Python website, https://www.python.org/

[180] Rodriguez Yakushev A, Jeuring J, Jansson P, Gerdes A, Kiselyov O, Oliveira BCdS (2008) Comparing libraries for generic programming in Haskell. In: Haskell Symposium, pp 111-122

[181] Rodriguez Yakushev A, Holdermans S, Löh A, Jeuring J (2009) Generic programming with fixed points for mutually recursive datatypes. In: Hutton G, Tolmach AP (eds) International Conference on Functional Programming, pp 233-244

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

[183] Schröder E (1895) Vorlesungen über die Algebra der Logik, vol 3. Taubner

[184] Schuman SA (ed) (1975) New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d'Informatique et d'Automatique

[185] Schuman SA (ed) (1976) New Directions in Algorithmic Languages, Prepared for IFIP Working Group 2.1 on Algol, Institut de Recherche d'Informatique et d'Automatique

[186] Sintzoff M (2003) On the design of correct and optimal dynamical systems and games. Information Processing Letters 88(1-2):59-65, DOI 10.1016/S0020-0190(03)00387-9
[187] Sintzoff S (2008) Synthesis of optimal control policies for some infinite-state transition systems. In: Audebaud P, Paulin-Mohring C (eds) Mathematics of Program Construction, Springer, Lecture Notes in Computer Science, vol 5133, pp 336–359, DOI 10.1007/978-3-540-70594-9_18

[188] Smith DR (1990) KIDS: A semiautomatic program development system. IEEE Transaction on Software Engineering 16(9):1024–1043, DOI 10.1109/32.58788

[189] Spivey JM (1990) A functional theory of exceptions. Science of Computer Programming 14(1):25–42, DOI 10.1016/0167-6423(90)90056-J

[190] Swierstra D, de Moor O (1993) Virtual data structures. In: Möller B, Partsch H, Schuman S (eds) Formal Program Development, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 355–371, DOI 10.1007/3-540-57499-9_26

[191] Swierstra SD, Duponcheel L (1996) Deterministic, error-correcting combinator parsers. In: Launchbury J, Meijer E, Sheard T (eds) Advanced Functional Programming, Springer, Lecture Notes in Computer Science, vol 1129, pp 184–207, DOI 10.1007/3-540-61628-4_7

[192] Swierstra W (2008) A functional specification of effects. PhD thesis, University of Nottingham

[193] Swierstra W, Alpuim J (2016) From proposition to program. In: Kiselyov O, King A (eds) Functional and Logic Programming, Springer International Publishing, Cham, pp 29–44

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

[195] Swierstra W, Baanen T (2019) A predicate transformer semantics for effects (functional pearl). Proceedings of the ACM on Programming Languages 3(ICFP):1–26

[196] Tafliovich A, Hehner ECR (2006) Quantum predicative programming. In: Uustalu T (ed) Mathematics of Program Construction, Springer, Lecture Notes in Computer Science, vol 4014, pp 433–454, DOI 10.1007/11783596_25

[197] Tarski A (1941) On the calculus of relations. Journal of Symbolic Logic 6(3):73–89, DOI 10.2307/2268577

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

[199] Uustalu T, Vene V (2008) Comonadic notions of computation. Electronic Notes in Theoretical Computer Science 203(5):263–284, DOI 10.1016/j.entcs.2008.05.029

[200] Uustalu T, Vene V, Pardo A (2001) Recursion schemes from comonads. Nordic Journal of Computing 8(3):366–390

[201] Wadler P (1990) Comprehending monads. In: LISP and Functional Programming, ACM, p 6178, DOI 10.1145/91556.91592

[202] Wadler P (1992) The essence of functional programming. In: Principles of Programming Languages, ACM, p 114, DOI 10.1145/143165.143169

[203] Wadler P (2015) Propositions as types. Communications of the ACM 58(12):75–84
[204] Wile D (1981) POPART: producer of parsers and related tools: System builder's manual. Tech. rep., USC/ISI Information Science Institute, University of Southern California

[205] Wile D (1981) Program developments as formal objects. Tech. rep., USC/ISI Information Science Institute, University of Southern California

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