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.2.0.tar.gz
sha512=733b02178722d2acc0b50d62139635261e9aaf36de58a997f0546ee5fb3e31bc537c637ba19577516c5ecfa3e8a3a206ea57c79b65a9478305a225720ebab278

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-04-12 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: 12 Apr 2024

Dependencies

None

Dev Dependencies (2)

  1. coq-stdpp (= "1.10.0") | (= "dev")
  2. coq (>= "8.18" & < "8.20~") | (= "dev")

Used by (3)

  1. coq-iris-heap-lang = "4.2.0"
  2. coq-vst >= "3.0beta2"
  3. coq-vst-iris

Conflicts

None