-
Notifications
You must be signed in to change notification settings - Fork 5
/
meta.yml
179 lines (131 loc) · 6.22 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
fullname: Hoare Type Theory
shortname: htt
organization: imdea-software
opam_name: coq-htt
community: false
action: true
dune: true
coqdoc: false
synopsis: >-
Hoare Type Theory
description: |-
Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
programs based on Separation logic.
HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A
Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition
`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads,
as used in the programming language Haskell. Monads hygienically combine the language features
for pure functional programming, with those for imperative programming, such as state or
exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard
isomorphism between monads and (functional programming variant of) Separation logic. Every
effectful command in HTT has a type that corresponds to the appropriate non-structural inference
rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a
command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for
sequential composition, and the type for monadic unit combines the Hoare rules for the idle
program (in a small-footprint variant) and for variable assignment (adapted for functional
variables). The connection reconciles dependent types with effects of state and exceptions and
establishes Separation logic as a type theory for such effects. In implementation terms, it means
that HTT implements Separation logic as a shallow embedding in Coq.
build: |-
## Building and installation instructions
The easiest way to install the latest released version of Hoare Type Theory
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-htt
```
To instead build and install manually, do:
``` shell
git clone https://github.com/imdea-software/htt.git
cd htt
dune build
dune install htt
```
If you also want to build the examples, run `make` instead of `dune`.
authors:
- name: Aleksandar Nanevski
initial: true
- name: Germán Andrés Delbianco
initial: false
- name: Alexander Gryzlov
initial: false
publications:
- pub_url: https://software.imdea.org/~aleks/papers/reflect/reflect.pdf
pub_title: Structuring the verification of heap-manipulating programs
pub_doi: 10.1145/1706299.1706331
maintainers:
- name: Alexander Gryzlov
nickname: clayrat
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: Apache-2.0
identifier: Apache-2.0
file: LICENSE
supported_coq_versions:
text: Coq 8.15 to 8.17
opam: '{ (>= "8.15" & < "8.19~") | (= "dev") }'
tested_coq_opam_versions:
- version: '1.17.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.18'
repo: 'mathcomp/mathcomp'
# - version: 'coq-dev'
# repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "1.17.0" & < "1.18~") | (= "dev") }'
description: |-
[MathComp ssreflect 1.17](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-fcsl-pcm
version: '{ (>= "1.8.0" & < "1.9~") | (= "dev") }'
description: |-
[FCSL-PCM 1.8](https://github.com/imdea-software/fcsl-pcm)
namespace: htt
keywords:
- name: partial commutative monoids
- name: separation logic
categories:
- name: Computer Science/Data Types and Data Structures
documentation: |-
## History
The original version of HTT can be found [here](https://software.imdea.org/~aleks/htt/).
## References
* [Dependent Type Theory of Stateful Higher-Order Functions](https://software.imdea.org/~aleks/papers/hoarelogic/depstate.pdf)
Aleksandar Nanevski and Greg Morrisett. Technical report TR-24-05, Harvard University, 2005.
* [Polymorphism and Separation in Hoare Type Theory](http://software.imdea.org/~aleks/htt/icfp06.pdf)
Aleksandar Nanevski, Greg Morrisett and Lars Birkedal. ICFP 2006.
The first paper containing a (very impoverished) definition of HTT.
* [Hoare Type Theory, Polymorphism and Separation](http://software.imdea.org/~aleks/htt/jfpsep07.pdf)
Aleksandar Nanevski, Greg Morrisett and Lars Birkedal. JFP 2007.
Journal version of the ICFP 2006 paper.
* [Abstract Predicates and Mutable ADTs in Hoare Type Theory](http://software.imdea.org/~aleks/htt/esop07.pdf)
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal. ESOP 2007.
Adding abstract predicates to HTT.
* [A Realizability Model for Impredicative Hoare Type Theory](http://software.imdea.org/~aleks/htt/esop08.pdf)
Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett. ESOP 2008.
A semantic model for HTT, but without large sigma types.
* [Ynot: Dependent Types for Imperative Programs](http://software.imdea.org/~aleks/htt/ynot08.pdf)
Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal. ICFP 2008.
First implementation of HTT as a DSL in Coq, and a number of examples.
* [Structuring the Verification of Heap-Manipulating Programs](http://software.imdea.org/~aleks/htt/reflect.pdf)
Aleksandar Nanevski, Viktor Vafeiadis and Josh Berfine. POPL 2010.
This paper introduces what is closest to the current structure of the implementation of HTT.
It puts emphasis on structuring programs and proofs together, rather than on attacking the
verification problem using proof automation. It carries out a large case study, verifying the
congruence closure algorithm of the Barcelogic SAT solver.
The current implementation differs from what's explained in this paper, in that it uses unary,
rather than binary postconditions.
* [Partiality, State and Dependent Types](http://software.imdea.org/~aleks/htt/tlca11.pdf)
Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. TLCA 2011.
A semantic model for HTT, with large sigma types.