-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
238 lines (228 loc) · 19.4 KB
/
index.html
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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="generator" content="rustdoc">
<title>Language-Integrated Verification</title>
<link href="./css/bootstrap.css" rel="stylesheet">
<link href="./css/bootstrap-theme.css" rel="stylesheet">
<link rel="stylesheet" type="text/css" href="./css/rust-book-slides.css">
<link rel="stylesheet" type="text/css" href="./css/editor-slides.css">
<style type="text/css">code{white-space: pre;}</style>
<style type="text/css">
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode {
margin: 0; padding: 0; vertical-align: baseline; border: none; }
table.sourceCode { width: 100%; line-height: 100%; }
td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; }
td.sourceCode { padding-left: 5px; }
code > span.kw { color: #007020; font-weight: bold; }
code > span.dt { color: #902000; }
code > span.dv { color: #40a070; }
code > span.bn { color: #40a070; }
code > span.fl { color: #40a070; }
code > span.ch { color: #4070a0; }
code > span.st { color: #4070a0; }
code > span.co { color: #60a0b0; font-style: italic; }
code > span.ot { color: #007020; }
code > span.al { color: #ff0000; font-weight: bold; }
code > span.fu { color: #06287e; }
code > span.er { color: #ff0000; font-weight: bold; }
</style>
</head>
<body class="rustdoc">
<div id='toc' class='mobile-hidden'>
</div>
<div id='page'>
<h1 style="border-bottom:none">Language-Integrated Verification</b>
<h2 style="border-bottom:none"></h2>
<h4 style="border-bottom: 2px solid #ddd"><i>Ranjit Jhala</i></h4>
<br>
<p><a href="book.pdf">[PDF]</a></p>
<ul class='chapter'>
<li><a href='01-intro.html'><b>1.</b>Follow Along at This URL</a></li>
<ul class='section'>
<li><a href='01-intro.html#whats-this'><b>1.1.</b> Whats this?</a></li>
<li><a href='01-intro.html#the-first-bug'><b>1.2.</b> The First <em>Bug</em></a></li>
<li><a href='01-intro.html#fast-forward-to-present-day'><b>1.3.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#fast-forward-to-present-day-1'><b>1.4.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#fast-forward-to-present-day-2'><b>1.5.</b> Fast forward to Present Day</a></li>
<li><a href='01-intro.html#programming-languages-research'><b>1.6.</b> Programming Languages Research</a></li>
<li><a href='01-intro.html#modern-languages'><b>1.7.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-1'><b>1.8.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-2'><b>1.9.</b> Modern Languages</a></li>
<li><a href='01-intro.html#modern-languages-3'><b>1.10.</b> Modern Languages?</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong'><b>1.11.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong-1'><b>1.12.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#well-typed-programs-can-go-very-wrong-2'><b>1.13.</b> Well-typed programs can go very wrong!</a></li>
<li><a href='01-intro.html#goal-language-integrated-verification'><b>1.14.</b> Goal: Language-Integrated Verification</a></li>
<li><a href='01-intro.html#goal-language-integrated-verification-1'><b>1.15.</b> Goal: Language-Integrated Verification</a></li>
<li><a href='01-intro.html#outline'><b>1.16.</b> Outline</a></li>
<li><a href='01-intro.html#outline-1'><b>1.17.</b> Outline</a></li>
<li><a href='01-intro.html#outline-2'><b>1.18.</b> Outline</a></li>
<li><a href='01-intro.html#outline-3'><b>1.19.</b> Outline</a></li>
<li><a href='01-intro.html#outline-4'><b>1.20.</b> Outline</a></li>
<li><a href='01-intro.html#outline-5'><b>1.21.</b> Outline</a></li>
</ul>
<li><a href='02-refinements.html'><b>2.</b>Simple Refinement Types</a></li>
<ul class='section'>
<li><a href='02-refinements.html#types'><b>2.1.</b> Types</a></li>
<li><a href='02-refinements.html#predicates'><b>2.2.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-1'><b>2.3.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-2'><b>2.4.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-3'><b>2.5.</b> Predicates</a></li>
<li><a href='02-refinements.html#predicates-4'><b>2.6.</b> Predicates</a></li>
<li><a href='02-refinements.html#example-singletons'><b>2.7.</b> Example: Singletons</a></li>
<li><a href='02-refinements.html#example-natural-numbers'><b>2.8.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#a-term-can-have-many-types'><b>2.9.</b> A Term Can Have <em>Many</em> Types</a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs'><b>2.10.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs-1'><b>2.11.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#predicate-subtyping-nuprl-pvs-2'><b>2.12.</b> 1. Predicate Subtyping <a href="http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf">[NUPRL, PVS]</a></a></li>
<li><a href='02-refinements.html#example-natural-numbers-1'><b>2.13.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#example-natural-numbers-2'><b>2.14.</b> Example: Natural Numbers</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls'><b>2.15.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-1'><b>2.16.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-2'><b>2.17.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#typing-applications-function-calls-3'><b>2.18.</b> 2. Typing Applications (Function Calls)</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101'><b>2.19.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101-1'><b>2.20.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#recap-refinement-types-101-2'><b>2.21.</b> Recap: Refinement Types 101</a></li>
<li><a href='02-refinements.html#outline'><b>2.22.</b> Outline</a></li>
<li><a href='02-refinements.html#outline-1'><b>2.23.</b> Outline</a></li>
</ul>
<li><a href='03-examples.html'><b>3.</b>Refinement Types by Example</a></li>
<ul class='section'>
<li><a href='03-examples.html#refinement-types-by-example-1'><b>3.1.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#refinement-types-by-example-2'><b>3.2.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#refinement-types-by-example-3'><b>3.3.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#specifications-pre-conditions'><b>3.4.</b> Specifications: Pre-Conditions</a></li>
<li><a href='03-examples.html#specifications-post-conditions'><b>3.5.</b> Specifications: Post-Conditions</a></li>
<li><a href='03-examples.html#refinement-types-by-example-4'><b>3.6.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#verification-vector-sum'><b>3.7.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#verification-vector-sum-1'><b>3.8.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#verification-vector-sum-2'><b>3.9.</b> Verification: Vector Sum</a></li>
<li><a href='03-examples.html#refinement-types-by-example-5'><b>3.10.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#inference'><b>3.11.</b> Inference</a></li>
<li><a href='03-examples.html#inference-vector-sum'><b>3.12.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-1'><b>3.13.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-2'><b>3.14.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-3'><b>3.15.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-4'><b>3.16.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#inference-vector-sum-5'><b>3.17.</b> Inference: Vector Sum</a></li>
<li><a href='03-examples.html#refinement-types-by-example-6'><b>3.18.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#collections-higher-order-functions'><b>3.19.</b> Collections & Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-1'><b>3.20.</b> Collections & Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-2'><b>3.21.</b> Collections & Higher-Order Functions</a></li>
<li><a href='03-examples.html#collections-higher-order-functions-3'><b>3.22.</b> Collections & Higher-Order Functions</a></li>
<li><a href='03-examples.html#refinement-types-by-example-7'><b>3.23.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#example-list-average'><b>3.24.</b> Example: List <code>average</code></a></li>
<li><a href='03-examples.html#refinements-for-datatypes'><b>3.25.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#measures-yield-refined-constructors'><b>3.26.</b> Measures Yield Refined Constructors</a></li>
<li><a href='03-examples.html#example-map-over-lists'><b>3.27.</b> Example: <code>map</code> over Lists</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-1'><b>3.28.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-2'><b>3.29.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinements-for-datatypes-3'><b>3.30.</b> Refinements for Datatypes</a></li>
<li><a href='03-examples.html#refinement-types-by-example-8'><b>3.31.</b> Refinement Types by Example</a></li>
<li><a href='03-examples.html#outline'><b>3.32.</b> Outline</a></li>
<li><a href='03-examples.html#outline-1'><b>3.33.</b> Outline</a></li>
</ul>
<li><a href='04-abstracting.html'><b>4.</b>Invariants In Constructors</a></li>
<ul class='section'>
<li><a href='04-abstracting.html#invariants-in-constructors-1'><b>4.1.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#invariants-in-constructors-2'><b>4.2.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#invariants-in-constructors-3'><b>4.3.</b> Invariants In Constructors</a></li>
<li><a href='04-abstracting.html#abstracting-refinements'><b>4.4.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#abstracting-refinements-1'><b>4.5.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#abstracting-refinements-2'><b>4.6.</b> Abstracting Refinements</a></li>
<li><a href='04-abstracting.html#using-abstract-refinements'><b>4.7.</b> Using Abstract Refinements</a></li>
<li><a href='04-abstracting.html#recap'><b>4.8.</b> Recap</a></li>
<li><a href='04-abstracting.html#recap-1'><b>4.9.</b> Recap</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type'><b>4.10.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-1'><b>4.11.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-2'><b>4.12.</b> Bounded Refinements: Induction as a Type</a></li>
<li><a href='04-abstracting.html#bounded-refinements-induction-as-a-type-3'><b>4.13.</b> Bounded Refinements: Induction as a Type</a></li>
</ul>
<li><a href='04-termination.html'><b>5.</b>Avoiding Infinite Loops</a></li>
<ul class='section'>
<li><a href='04-termination.html#example-proving-termination-of-sum'><b>5.1.</b> Example: Proving Termination of <code>sum</code></a></li>
<li><a href='04-termination.html#proving-termination'><b>5.2.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-1'><b>5.3.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-2'><b>5.4.</b> Proving Termination</a></li>
<li><a href='04-termination.html#proving-termination-3'><b>5.5.</b> Proving Termination</a></li>
<li><a href='04-termination.html#example-proving-termination-of-sum-1'><b>5.6.</b> Example: Proving Termination of <code>sum</code></a></li>
<li><a href='04-termination.html#user-specified-termination-metrics'><b>5.7.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#user-specified-termination-metrics-1'><b>5.8.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#user-specified-termination-metrics-2'><b>5.9.</b> User Specified Termination Metrics</a></li>
<li><a href='04-termination.html#proving-termination-4'><b>5.10.</b> Proving Termination</a></li>
<li><a href='04-termination.html#lexicographic-termination'><b>5.11.</b> Lexicographic Termination</a></li>
<li><a href='04-termination.html#how-about-data-types'><b>5.12.</b> How About Data Types?</a></li>
<li><a href='04-termination.html#user-specified-metrics-on-data-types'><b>5.13.</b> User specified metrics on Data Types</a></li>
<li><a href='04-termination.html#termination-can-be-tricky'><b>5.14.</b> Termination Can be Tricky</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-1'><b>5.15.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-2'><b>5.16.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-3'><b>5.17.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-4'><b>5.18.</b> Avoiding Infinite Loops</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice'><b>5.19.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-1'><b>5.20.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-2'><b>5.21.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#avoiding-infinite-loops-is-easy-in-practice-3'><b>5.22.</b> Avoiding Infinite Loops is Easy (in Practice)</a></li>
<li><a href='04-termination.html#outline'><b>5.23.</b> Outline</a></li>
<li><a href='04-termination.html#outline-1'><b>5.24.</b> Outline</a></li>
</ul>
<li><a href='05-reflection.html'><b>6.</b>Types as Theorems, Programs as Proofs</a></li>
<ul class='section'>
<li><a href='05-reflection.html#types-as-theorems'><b>6.1.</b> Types As Theorems</a></li>
<li><a href='05-reflection.html#types-as-theorems-example'><b>6.2.</b> Types as Theorems: Example</a></li>
<li><a href='05-reflection.html#programs-as-proofs-example'><b>6.3.</b> Programs As Proofs: Example</a></li>
<li><a href='05-reflection.html#types-as-theorems-1'><b>6.4.</b> Types As Theorems</a></li>
<li><a href='05-reflection.html#types-as-theorems-example-1'><b>6.5.</b> Types as Theorems: Example</a></li>
<li><a href='05-reflection.html#programs-as-proofs-example-1'><b>6.6.</b> Programs As Proofs: Example</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-1'><b>6.7.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#those-proofs-were-boring'><b>6.8.</b> Those Proofs were Boring</a></li>
<li><a href='05-reflection.html#those-proofs-were-boring-1'><b>6.9.</b> Those Proofs were Boring</a></li>
<li><a href='05-reflection.html#theorems-about-functions'><b>6.10.</b> Theorems about Functions</a></li>
<li><a href='05-reflection.html#refinement-reflection'><b>6.11.</b> Refinement Reflection</a></li>
<li><a href='05-reflection.html#reflect-function-into-output-type'><b>6.12.</b> Reflect Function into Output Type</a></li>
<li><a href='05-reflection.html#reflect-function-into-output-type-1'><b>6.13.</b> Reflect Function into Output Type</a></li>
<li><a href='05-reflection.html#reflection-at-result-type'><b>6.14.</b> Reflection at Result Type</a></li>
<li><a href='05-reflection.html#structuring-proofs-as-calculations'><b>6.15.</b> Structuring Proofs as Calculations</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-2'><b>6.16.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas'><b>6.17.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas-1'><b>6.18.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#reusing-proofs-functions-as-lemmas-2'><b>6.19.</b> Reusing Proofs: Functions as Lemmas</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-3'><b>6.20.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-4'><b>6.21.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation'><b>6.22.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation-1'><b>6.23.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-logical-evaluation-2'><b>6.24.</b> Proof by Logical Evaluation</a></li>
<li><a href='05-reflection.html#proof-by-induction'><b>6.25.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#proof-by-induction-1'><b>6.26.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#proof-by-induction-2'><b>6.27.</b> Proof by Induction</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-5'><b>6.28.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-6'><b>6.29.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-7'><b>6.30.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#theorems-about-data'><b>6.31.</b> Theorems about Data</a></li>
<li><a href='05-reflection.html#theorems-about-data-associativity-of-append'><b>6.32.</b> Theorems about Data: Associativity of <code>append</code></a></li>
<li><a href='05-reflection.html#case-study-mapreduce'><b>6.33.</b> Case Study: MapReduce</a></li>
<li><a href='05-reflection.html#case-study-mapreduce-1'><b>6.34.</b> Case Study: MapReduce</a></li>
<li><a href='05-reflection.html#reduce-theorem'><b>6.35.</b> Reduce Theorem</a></li>
<li><a href='05-reflection.html#types-as-theorems-programs-as-proofs-8'><b>6.36.</b> Types as Theorems, Programs as Proofs</a></li>
<li><a href='05-reflection.html#outline'><b>6.37.</b> Outline</a></li>
<li><a href='05-reflection.html#outline-1'><b>6.38.</b> Outline</a></li>
</ul>
<li><a href='06-concl.html'><b>7.</b>LiquidHaskell</a></li>
<ul class='section'>
<li><a href='06-concl.html#liquidhaskell-1'><b>7.1.</b> LiquidHaskell</a></li>
<li><a href='06-concl.html#liquidhaskell-2'><b>7.2.</b> LiquidHaskell</a></li>
<li><a href='06-concl.html#evaluation'><b>7.3.</b> Evaluation</a></li>
<li><a href='06-concl.html#recap-refinement-types'><b>7.4.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-1'><b>7.5.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-2'><b>7.6.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#recap-refinement-types-3'><b>7.7.</b> Recap: Refinement Types</a></li>
<li><a href='06-concl.html#many-friends-many-directions'><b>7.8.</b> Many Friends, Many Directions</a></li>
<li><a href='06-concl.html#thank-you'><b>7.9.</b> Thank You!</a></li>
</ul>
</ul>
</div>
</body>
</html>