package coq-iris

  1. Overview
  2. No Docs
A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs

Install

Dune Dependency

iris-project.org Edit opam file Versions (11)

Authors

  1. T
    The Iris Team

Maintainers

  1. R
    Ralf Jung <jung@mpi-sws.org>

Sources

iris-3.6.0.tar.gz
sha512=6b9871a299e0e97d4cc3466e3b1c11c07af4ae2c5249f64ecdbd88d813e6382cb56bb6f041e52b5dc1a0c5f6f2f5995b1f7b5f1cdcc7be3336fccaf8fb046503

Description

Iris is a framework for reasoning about the safety of concurrent programs using concurrent separation logic. It can be used to develop a program logic, for defining logical relations, and for reasoning about type systems, among other applications. This package includes the base logic, Iris Proof Mode (IPM) / MoSeL, and a general language-independent program logic; see coq-iris-heap-lang for an instantiation of the program logic to a particular programming language.

Tags

date:2022-01-22 logpath:iris.prelude logpath:iris.algebra logpath:iris.si_logic logpath:iris.bi logpath:iris.proofmode logpath:iris.base_logic logpath:iris.program_logic

Published: 23 Jan 2022

Dependencies

None

Dev Dependencies (2)

  1. coq-stdpp (= "1.7.0") | (= "dev")
  2. coq (>= "8.13" & < "8.17~") | (= "dev")

Used by (2)

  1. coq-iris-heap-lang = "3.6.0"
  2. coq-katamaran >= "0.2.0"

Conflicts

None