Logical relations (WIP)

<font color=“red”>this page is currently under construction</font>

Logical relations in Iris

Here you can find a formalization of logical relations in Iris for a variant of System F with existential types (mini-modules), general recursion, higher-order store, and concurrency.

The formalization provides a sort of calculus for proving logical refinement (and, consequently, observational refinements, aka linearizability); there is a number of examples:

Documentation is coming soon…

Other stuff

Last updated: 2017-10-06 vr 10:26

Emacs 25.1.1 (Org mode 9.0.9)

Validate