Logical relations (WIP)

this page is currently under construction

Logical relations in Iris

Here you can find a formalization of logical relations in Iris for a variant of System F with existential types (modules-light), 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-22 zo 12:13

Emacs 25.1.1 (Org mode 9.0.9)

Validate