coq-arl.opam

opam-version: "2.0"
maintainer: "traian.serbanuta@gmail.com"
version: "dev"

homepage: "https://github.com/traiansf/coq-arl"
dev-repo: "git+https://github.com/traiansf/coq-arl.git"
bug-reports: "https://github.com/traiansf/coq-arl/issues"
license: "MIT"

synopsis: "Coq formalization of Abstract Reachability Logic"
description: """
Formalization of Abstract Reachability Logic, containing a formalization
of abstract transition systems together with a notion of
CTL-like always-finally reachability claims and an abstract deduction system
which can be used to derive such claims.
The formalization is next extended to handle (abstract) quantification.
"""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.15"}
  "coq-stdpp" {>= "1.7.0" & < "1.8.0"}
  "coq-sets" {= "dev"}
]

tags: [
  "keyword:abstract rewrite system"
  "keyword:reachability"
  "keyword:ctl"
]
authors: [
  "Traian Florin Șerbănuță"
]