[Agda] [TYPES] Progress + Preservation = Evaluation

[Nils Anders Danielsson]

On 2018-07-07 00:45, Philip Wadler wrote:
> Indeed, I considered using Delay for the evaluator in the textbook,
> but decided that supplying a step count was simpler, and avoided the
> need to explain coinduction.

In "Operational Semantics Using the Partiality Monad"
(https://doi.org/10.1145/2364527.2364546) I defined the semantics of an
untyped language by giving a definitional interpreter, using the delay
monad. Then I proved type soundness for this language as a negative
statement (using a more positive lemma):

   [] ⊢ t ∈ σ → ¬ (⟦ t ⟧ [] ≈ fail)

Thus, instead of starting with type soundness and deriving an evaluator,
I started with an evaluator and proved type soundness.

This kind of exercise has also been performed using fuel, see Siek's
"Type Safety in Three Easy Lemmas"
(http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html)
and "Functional Big-Step Semantics" by Owens et al.
(https://doi.org/10.1007/978-3-662-49498-1_23).

-- 
/NAD