Skip to content

Remove many variants of logical relations

Robbert Krebbers requested to merge robbert/logrel into master

This MR removes the logical relations for stlc, F_mu, and F_mu_ref, and only keeps the one for the most expressive language F_mu_ref_conc.

Moreover, it puts this logical relation, together with the one for heaplang, in the logrel folder.

This MR makes porting iris-examples after changes to Iris updates much easier---the same work often had to be redone for all versions of the logical relation.

/cc @amintimany

Edited by Robbert Krebbers

Merge request reports