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.0.0.tar.gz
sha512=919ab6a7657d7bc6df3be576a752df884e44b638318574fcf0682cc04be3a272270986fb23a0010b09b4fd80c6a0dafe04b7364764381e6831e81e1f942ebffc

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-08-17 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: 18 Aug 2022

Dependencies

None

Dev Dependencies (2)

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

Conflicts

None