[Agda] [TYPES] Progress + Preservation = Evaluation

[Roman]

> avoided the need to explain coinduction

Conor uses a constructive free monad. So coinduction is just one
interpretation and you can avoid it and present only the fuel-driven
execution semantics. Though, if it's the only one you need, why
complicate it by using free monads indeed.

There is a very remotely related topic to what you're asking, it's
called Normalization by Completeness. Here are some slides: [1]. In
essence, you can get normalization by composing Soundness with
Completeness which is kinda related, because Progress and Preservation
are forms of Soundness and Completeness (I always forget which one is
which). But there Soundness means Evaluation (to a value in some
model) and Completeness means Reification, so I'm not really sure
whether there is any relation at all.

[1] http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf

Best regards,
Roman