This is a logical relations case study in Iris for the CIS 670 course at UPenn.
proposal/contains an abstract for the projectsrc/(WIP) logical relations in Iris for CBPVstlc/simple logical relation with stlc with recursive types based on https://gitlab.mpi-sws.org/iris/examples/-/tree/master/theories/logrel