|
| 1 | +opam-version: "2.0" |
| 2 | + |
| 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"} |
| 34 | + "coq-mathcomp-ssreflect" {>= "2.2.0"} |
| 35 | + "coq-hierarchy-builder" {>= "1.7.0"} |
| 36 | + "coq-mathcomp-algebra" |
| 37 | + "coq-mathcomp-fingroup" |
| 38 | + "coq-fcsl-pcm" {>= "2.1.0"} |
| 39 | + "coq-htt-core" {= version} |
| 40 | +] |
| 41 | + |
| 42 | +tags: [ |
| 43 | + "category:Computer Science/Data Types and Data Structures" |
| 44 | + "keyword:partial commutative monoids" |
| 45 | + "keyword:separation logic" |
| 46 | + "logpath:htt" |
| 47 | +] |
| 48 | + |
| 49 | +authors: [ |
| 50 | + "Aleksandar Nanevski" |
| 51 | + "Germán Andrés Delbianco" |
| 52 | + "Alexander Gryzlov" |
| 53 | + "Marcos Grandury" |
| 54 | +] |
| 55 | + |
| 56 | +url { |
| 57 | + src: "git+https://github.com/imdea-software/htt.git#master" |
| 58 | +} |
| 59 | + |
0 commit comments