Skip to content
Snippets Groups Projects
Select Git revision
  • master default
  • no-bi-canonical
  • basic-dune
  • inv_exc_0_ipm
  • fix-497-hint-immediate
  • notations
  • later-credits-drop
  • bi_pure_scopes
  • fupd-commutes
  • periscopes-v2
  • periscopes
  • paolo/tc-strict-resolution-backport
  • doc-equalities
  • ascii-sections
  • fix-notation
  • explicit-vdash
  • more-convenient-fupd_proper
  • test-bigop-synchanges
  • later_impl_experiments
  • later_impl_test
  • 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
Compare
Forked from Iris / Iris
5402 commits behind the upstream repository.
user avatar
Cancelable and IdFree typeclasses.
Jacques-Henri Jourdan authored 
Cancelable elements are a new way of proving local updates, by
removing some cancellable element of the global state, provided that
we own it and we are willing to lose this ownership.

Identity-free elements are an auxiliary that is necessary to prove that
[Some x] is cancelable.

For technical reasons, these two notions are not defined exactly like
what one might expect, but also take into account validity. Otherwise,
an exclusive element would not be cancelable or idfree, which is
rather confusing.
71c10187
History
user avatar 71c10187
History
Name Last commit Last update
benchmark
build
docs
theories
.gitignore
.gitlab-ci.yml
CHANGELOG.md
LICENSE
LICENSE-CODE
LICENSE-DOCS
Makefile
ProofMode.md
README.md
_CoqProject
awk.Makefile
naming.txt
opam
opam.pins
README.md

IRIS COQ DEVELOPMENT

This is the Coq development of the Iris Project.

Prerequisites

This version is known to compile with:

  • Coq 8.6
  • Ssreflect 1.6.1

The easiest way to install the correct versions of the dependencies is through opam. Coq packages are available on the coq-released repository, set up by the command:

opam repo add coq-released https://coq.inria.fr/opam/released

Once you got opam set up, just run make build-dep to install the right versions of the dependencies. When the dependencies change, just run make build-dep again.

If you need to work with Coq 8.5, please check out the iris-3.0 branch.

Building Instructions

Run make to build the full development.

Structure

  • The folder prelude contains an extended "Standard Library" by Robbert Krebbers.
  • The folder algebra contains the COFE and CMRA constructions as well as the solver for recursive domain equations.
  • The folder base_logic defines the Iris base logic and the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources.
    • The subfolder lib contains some generally useful derived constructions. Most importantly, it defines composeable dynamic resources and ownership of them; the other constructions depend on this setup.
  • The folder program_logic specializes the base logic to build Iris, the program logic. This includes weakest preconditions that are defined for any language satisfying some generic axioms, and some derived constructions that work for any such language.
  • The folder proofmode contains the Iris proof mode, which extends Coq with contexts for persistent and spatial Iris assertions. It also contains tactics for interactive proofs in Iris. Documentation can be found in ProofMode.md.
  • The folder heap_lang defines the ML-like concurrent heap language
  • The folder tests contains modules we use to test our infrastructure. Users of the Iris Coq library should not depend on these modules; they may change or disappear without any notice.

Documentation

A LaTeX version of the core logic definitions and some derived forms is available in docs/iris.tex. A compiled PDF version of this document is available online.