4 ms·

Have a pure model of memory which is implemented directly. Associate this with a proof that the extensional side of it is pure (copying mechanics of substructur

by tel 11y ago

Have a pure model of memory which is implemented directly. Associate this with a proof that the extensional side of it is pure (copying mechanics of substructural types) and you're done.

pron 11y ago
Right, but proving correctness would still be much harder than with the model checker, I think.