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.1.0.tar.gz
sha512=ce2c1523458f912dc64f9b962df65baf6efabb650fced27b302901374f50cfe818a80e0bf9c5cb465efa08ff9949126dc0b7d6603efc4151f78b76c5ce3bd676

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:2023-10-11 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: 11 Oct 2023

Dependencies

None

Dev Dependencies (2)

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

Conflicts

None