by Nils Anders Danielsson on November 30, 2010.
Tagged as: Lunches.
Previously we have discussed using the partiality monad to define operational semantics for partial languages. Last Friday I talked about how I have used sized types (in MiniAgda) to define a compatible program inequality relation on top of such a semantics. The definition I ended up with turned out to be quite similar to step-indexed logical relations.
Interested readers can have a look at the (very verbose) MiniAgda code.