Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.021Oct19181311754330Sep2618121031Aug2413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb272625242322212019Add missing type in a signature.fix compatibility with Coq 8.7Merge branch 'ralf/prophecy' into 'master'note some FIXMEsmore nitsuse 'proph' instead of a notation, and rename type of prophecy variables to proph_idmore nitsgeneralize to lists of observations per program stepfix nitsuse record for heap_lang stateMerge remote-tracking branch 'origin/master' into ralf/prophecy`(P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q)` holds for general BIs.fix typotest and support Coq 8.8.2Merge branch 'robbert/pure_exec_nsteps' into 'master'Add changelog entry for `PureExec`.Support multiple steps in `PureExec`.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqUse only printing on notations for lambdas.heap_lang consistent spellingchangelogwhitespace tweaksdocument some heap_lang design choicestweak WP def.n and fix eauto in heap_langfix nitschange prophecy notationfix heap_lang/total_adequacyremove failing part of coin_flip; remove atomic_snapshotProving ownp.v and including it back into the buildfix TWPMaking prophecy-related examples work with the new prophecy supportAdding support for prophecy variables to heap_langFinalizing general (not prophecy specific) support for observationsAdding initial support for observations to the definition of wp for later prophecy supportshrink proof of timestamp_subImplementing atomic-pair-snapshot example from Sergey et al. (ESOP'15)splitting up prophecy into separate fileSimpler proofFirst motivating example for prophecy variables (coin-flip)wp_fork changelog
Loading