Final version

[rolyp]

Minor corrections.

• Tidy-up pass over theorems/proofs #112
• acknowledgements
• L76 "to specified" -> "to be specified"
• L78 "to do allow" -> "to allow"
• L512 "turing" -> "turning"
• L775 "using using" -> "using"
• L776 "other that" -> "other than"
• L806: What about the ambient availability?
• L818 "form" -> "and for every input $\overrightarrow{n}$ form"
• line 75: require data transformations to be specified
• line 77: what we would like is to allow
• line 79: artefact as a baked-in
• line 178: our implementation is untyped
• line 180: structured data which are
• line 234: with --> being part of the notation
• line 240: allows us to transform an eliminator ... into an eliminator of
• line 370: varepsilon in the unit rule should be ()
• line 453: The figure is a preorder on values, not a partial order.
• line 457: please clarify the presentation of the two-point lattice, including which elements are in the set (rather than reusing "2")
• line 494: Figure 8 is a preorder
• line 510: In practice
• line 512: evaluation, turning input
• line 544: for the var case, perhaps use \top instead of tt, to be more generic
• line 555&556: in cons, I think kappas on the right should be kappa-prime
• line 903: again the name "2" is used for both the algebra and the carrier set. Just enumerate the elements of the carrier.
• L83: "As well as providing"
• line 1174: Related to this is work on Resugaring by Pombrio et al.
• L178: "implementation is untyped"
• L179: "types A and B**,** which"
• L179: "e : e'" has space before ":" but "x: e" does not. This seems inconsistent.
• L221: There is an extra space before both citations on this line.
• L282: There is an extra space before the citation on this line.
• L325: "figure**,** the"
• L490: "becomes selection" -> "become selections"
• L415: ", which are"