Merge Requests · Iris

Weakest preconditions for total program correctness 5 of 5 tasks completed

iris!65 · opened Sep 24, 2017 by Robbert Krebbers
- MERGED
- 69
updated Jan 18, 2018
Type classes for updates properties

iris!106 · opened Jan 15, 2018 by Jacques-Henri Jourdan gen_proofmode
- MERGED
- 18
updated Jan 18, 2018
Add a Notation for `sn`: strongly normalizing.

stdpp!25 · opened Jan 12, 2018 by Robbert Krebbers
- MERGED
- 1
updated Jan 13, 2018
Construct BI on monotone function spaces.

iris!92 · opened Nov 28, 2017 by Janno gen_proofmode
- MERGED
- 69
updated Dec 29, 2017
Consistent handling of pure implication and forall

iris!104 · opened Dec 20, 2017 by Robbert Krebbers T-proofmode
- MERGED
- 6
updated Dec 21, 2017
Type classes for fancy updates and basic updates.

iris!101 · opened Dec 11, 2017 by Jacques-Henri Jourdan gen_proofmode
- MERGED
- 12
updated Dec 14, 2017
Prove that uPred is complete even if we remove the validity restriction in uPred_closed.

iris!99 · opened Dec 06, 2017 by Jacques-Henri Jourdan Iris 3.1
- MERGED
- 21
updated Dec 08, 2017
Add atomic fetch-and-add operation to heap_lang

iris!96 · opened Dec 04, 2017 by Robbert Krebbers
- MERGED
- 2
updated Dec 05, 2017
Lattices notation for order, join, meet, top and bot.

stdpp!23 · opened Dec 04, 2017 by Jacques-Henri Jourdan
- MERGED
- 12
updated Dec 05, 2017
typeclass comments

stdpp!24 · opened Dec 05, 2017 by Ralf Jung
- MERGED
- 0
updated Dec 05, 2017
Use `simpl` in `wp_` tactics just in the expression

iris!94 · opened Nov 29, 2017 by Robbert Krebbers
- MERGED
- 5
updated Nov 30, 2017
Provide a pretty-printer for [nat].

stdpp!15 · opened Oct 31, 2017 by Ghost User
- MERGED
- 8
updated Nov 29, 2017
Make x.1, x.2 notation compatible with ssrfun.

stdpp!21 · opened Nov 29, 2017 by David Swasey
- MERGED
- 5
updated Nov 29, 2017
Allow compiling against "dev" version of Coq

stdpp!20 · opened Nov 29, 2017 by Ralf Jung
- MERGED
- 4
updated Nov 29, 2017
notation for declaring a function non-expansive

iris!42 · opened Jan 25, 2017 by Ralf Jung
- MERGED
- 9
updated Nov 28, 2017
Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod`

iris!88 · opened Nov 21, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 34
updated Nov 28, 2017
do not make use of wp_bind_inv unnecessarily

iris!87 · opened Nov 21, 2017 by Ralf Jung Iris 3.1
- MERGED
- 16
updated Nov 24, 2017
Use solely canonical structures for language hierarchy.

iris!90 · opened Nov 23, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 12
updated Nov 24, 2017
Fix some typos in Section 9.2 (Boxes) in the docs.

iris!89 · opened Nov 23, 2017 by Dan Frumin
- MERGED
- 1
updated Nov 23, 2017
Pattern matching notation for monadic binds

stdpp!18 · opened Nov 14, 2017 by Robbert Krebbers
- MERGED
- 9
updated Nov 22, 2017