Skip to content

Commit d8c2636

Browse files
palmskogpalmskog
authored
Merge pull request rocq-prover#3303 from aleksnanevski/master
releasing coq-htt-core and coq-htt 2.1.0
2 parents 0e4f54e + 85a8173 commit d8c2636

File tree

2 files changed

+117
-0
lines changed
  • released/packages
    • coq-htt-core/coq-htt-core.2.1.0
    • coq-htt/coq-htt.2.1.0

2 files changed

+117
-0
lines changed

‎released/packages/coq-htt-core/coq-htt-core.2.1.0/opam‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
opam-version: "2.0"
2+
maintainer: "fcsl@software.imdea.org"
3+
4+
homepage: "https://github.com/imdea-software/htt"
5+
dev-repo: "git+https://github.com/imdea-software/htt.git"
6+
bug-reports: "https://github.com/imdea-software/htt/issues"
7+
license: "Apache-2.0"
8+
9+
synopsis: "Hoare Type Theory"
10+
description: """
11+
Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
12+
programs based on Separation logic.
13+
14+
HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A
15+
Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition
16+
`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads,
17+
as used in the programming language Haskell. Monads hygienically combine the language features
18+
for pure functional programming, with those for imperative programming, such as state or
19+
exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard
20+
isomorphism between monads and (functional programming variant of) Separation logic. Every
21+
effectful command in HTT has a type that corresponds to the appropriate non-structural inference
22+
rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a
23+
command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for
24+
sequential composition, and the type for monadic unit combines the Hoare rules for the idle
25+
program (in a small-footprint variant) and for variable assignment (adapted for functional
26+
variables). The connection reconciles dependent types with effects of state and exceptions and
27+
establishes Separation logic as a type theory for such effects. In implementation terms, it means
28+
that HTT implements Separation logic as a shallow embedding in Coq."""
29+
30+
build: [make "-C" "htt" "-j%{jobs}%"]
31+
install: [make "-C" "htt" "install"]
32+
depends: [
33+
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
34+
"coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
35+
"coq-mathcomp-algebra"
36+
"coq-mathcomp-fingroup"
37+
"coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
38+
]
39+
40+
tags: [
41+
"category:Computer Science/Data Types and Data Structures"
42+
"keyword:partial commutative monoids"
43+
"keyword:separation logic"
44+
"logpath:htt"
45+
]
46+
47+
authors: [
48+
"Aleksandar Nanevski"
49+
"Germán Andrés Delbianco"
50+
"Alexander Gryzlov"
51+
"Marcos Grandury"
52+
]
53+
54+
url {
55+
src: "https://github.com/imdea-software/htt/archive/refs/tags/v2.1.0.tar.gz"
56+
checksum: "sha256=e2819211c05a011f8101d006865c642a513c3e581810f590d8d8d7a651046b05"
57+
}
58+

‎released/packages/coq-htt/coq-htt.2.1.0/opam‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
opam-version: "2.0"
2+
maintainer: "fcsl@software.imdea.org"
3+
4+
homepage: "https://github.com/imdea-software/htt"
5+
dev-repo: "git+https://github.com/imdea-software/htt.git"
6+
bug-reports: "https://github.com/imdea-software/htt/issues"
7+
license: "Apache-2.0"
8+
9+
synopsis: "Hoare Type Theory"
10+
description: """
11+
Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
12+
programs based on Separation logic.
13+
14+
HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A
15+
Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition
16+
`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads,
17+
as used in the programming language Haskell. Monads hygienically combine the language features
18+
for pure functional programming, with those for imperative programming, such as state or
19+
exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard
20+
isomorphism between monads and (functional programming variant of) Separation logic. Every
21+
effectful command in HTT has a type that corresponds to the appropriate non-structural inference
22+
rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a
23+
command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for
24+
sequential composition, and the type for monadic unit combines the Hoare rules for the idle
25+
program (in a small-footprint variant) and for variable assignment (adapted for functional
26+
variables). The connection reconciles dependent types with effects of state and exceptions and
27+
establishes Separation logic as a type theory for such effects. In implementation terms, it means
28+
that HTT implements Separation logic as a shallow embedding in Coq."""
29+
30+
build: [make "-C" "examples" "-j%{jobs}%"]
31+
install: [make "-C" "examples" "install"]
32+
depends: [
33+
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
34+
"coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
35+
"coq-mathcomp-algebra"
36+
"coq-mathcomp-fingroup"
37+
"coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
38+
"coq-htt-core" {= version}
39+
]
40+
41+
tags: [
42+
"category:Computer Science/Data Types and Data Structures"
43+
"keyword:partial commutative monoids"
44+
"keyword:separation logic"
45+
"logpath:htt"
46+
]
47+
48+
authors: [
49+
"Aleksandar Nanevski"
50+
"Germán Andrés Delbianco"
51+
"Alexander Gryzlov"
52+
"Marcos Grandury"
53+
]
54+
55+
url {
56+
src: "https://github.com/imdea-software/htt/archive/refs/tags/v2.1.0.tar.gz"
57+
checksum: "sha256=e2819211c05a011f8101d006865c642a513c3e581810f590d8d8d7a651046b05"
58+
}
59+

0 commit comments

Comments
 (0)