program_logic · 34f9f865c867b66d1e929b075fa55097d6b146b5 · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

6269 commits behind the upstream repository.

Simplify the counter example proof a bit.

Robbert Krebbers authored 8 years ago

Instead of having connectives pvs0 and pvs1 we now have one connective
pvs that is indexed by a Boolean.

c4054f80

c4054f80 8 years ago

Name	Last commit	Last update
..
adequacy.v
auth.v
boxes.v
counter_examples.v
ectx_language.v
ectx_lifting.v
ectxi_language.v
ghost_ownership.v
global_functor.v
hoare.v
invariants.v
iris.v
language.v
lifting.v
model.v
namespaces.v
ownership.v
pviewshifts.v
saved_prop.v
sts.v
weakestpre.v