Commit be23bc6a authored by Ralf Jung's avatar Ralf Jung
Browse files

update package descriptions

parent 12925885
......@@ -9,8 +9,12 @@ version: "dev"
synopsis: "The canonical example language for Iris"
description: """
This package provides the iris.heap_lang Coq module.
This package defines HeapLang, a concurrent lambda calculus with references, and
uses Iris to build a program logic for HeapLang programs.
tags: [
depends: [
"coq-iris" {= version}
......@@ -9,9 +9,22 @@ version: "dev"
synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
description: """
This package provides the following Coq modules:
iris.prelude, iris.algebra, iris.si_logic,, iris.proofmode, iris.base_logic, iris.program_logic.
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: [
depends: [
"coq" { (>= "8.12" & < "8.15~") | (= "dev") }
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment