[ old ] Written down version of Away Day'13 talk

I was focusing on the idea that by tweaking the model construction used
in Normalization by Evaluation, we can have different equational theories.

The typical model decides beta-xi-eta by having eta-long normal forms which
is known to be expensive but we can get only beta-xi (and eta expand lazily
when comparing two terms for equality) or even simply beta (i.e. doing only
weak-head normalization).
Of course, this presentation should be expanded to encompass the nu rules
we presented at DTP'13 because we manage to decide them by tweaking the
model too & the same sort of pattern emerge (e.g. reification at evaluation
time).