Eval/uneval Galois connection

[rolyp]

• remove traces from the codomain of eval in core calculus
• ditto implementation language
• sync with new syntax for definitions
• use function-space arrow for trie types; drop notion of “continuation type”
• typing of continuations should defer to either expression typing or trie typing
• revisit arrow direction for uneval, unmatch?
• defs should use annotations on variables, as per impl
• perhaps separately show how to interleave traces with values?
• prove matchFwd and matchBwd form a Galois connection
  • define matchFwd and matchBwd
  • fwd after bwd
  • bwd after bwd
• revisit non-determinism introduced by ⊒ notation – might need a new relation
• determinism lemmas (up to hole equivalence)
• prove eval and uneval form Galois connection
  • make the trace an index on the relation
  • define evalFwd and evalBwd (for each T)
  • formalise primitives broadly as implemented (Formalise primitives broadly as implemented #76)
  • switch to 1-D arrays (Switch to 1-dimensional arrays #77)
  • fwd after bwd
  • bwd after fwd
• state (prove?) required monotonicity lemmas – deal with this later
• “closeDefs” GC
  • state theorem
  • prove - Mutual recursion lemma #84