Size-indexed logical relations

November 30th, 2010 by Nils Anders Danielsson

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.

Leave a Reply