This fixes the abstract typing relation in the update semantics and the value relation between the update and value semantics for abstract types. Both of these relations were broken due to not taking the Cogent heap as an argument.
Before this fix, one could show that all pointers in an abstract value are valid, i.e. point to something, for all Cogent heaps, which is clearly incorrect.
This fixes the abstract typing relation in the update semantics and the value relation between the update and value semantics for abstract types. Both of these relations were broken due to not taking the Cogent heap as an argument.
Before this fix, one could show that all pointers in an abstract value are valid, i.e. point to something, for all Cogent heaps, which is clearly incorrect.
With these fixes, an additional constraint on abstract types is required, i.e. their values satisfy the frame constraint, in order to prove the uval_typing_frame and upd_val_rel_frame theorems. This addition should not adversely affect Cogent since this constraint is alluded to in "Type Systems for System Types", chapter 4, subsection "Abstract Values", page 88, (https://www.unsworks.unsw.edu.au/primo-explore/fulldisplay?docid=unsworks_61747&vid=UNSWORKS&search_scope=unsworks_search_scope&tab=default_tab&lang=en_US&context=L).