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-4.3.0.tar.gz
sha512=fcb1d2a9290931f4984cf20e1084876c221ec9f3022761bf6948ef7ce0f22b7babd3d70abddd6b96bcde2108746d23ff790e576db01aff6f2012e0a38ee74afa

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:2024-10-31 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: 31 Oct 2024

Dependencies

None

Dev Dependencies (2)

  1. coq-stdpp (= "1.11.0") | (= "dev")
  2. coq (>= "8.19" & < "8.21~") | (= "dev")

Conflicts

None