forked from sven--/Software-Foundations
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Review1.html
232 lines (149 loc) · 4.33 KB
/
Review1.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
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Review1: Review Session for First Midterm</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Review1<span class="subtitle">Review Session for First Midterm</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</div>
<div class="code code-tight">
<br/>
<br/>
</div>
<div class="doc">
<a name="lab357"></a><h1 class="section">General Notes</h1>
<div class="paragraph"> </div>
<a name="lab358"></a><h3 class="section">Standard vs. Advanced Exams</h3>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> Unlike the homework assignments, we will make up two completely
separate versions of the exam — a "standard exam" and an
"advanced exam." They will share some problems, but there will
be problems on each that are not on the other.
<div class="paragraph"> </div>
You can choose to take whichever one you want at the beginning
of the exam period.
</li>
</ul>
<div class="paragraph"> </div>
<a name="lab359"></a><h3 class="section">Grading</h3>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> Meaning of grades:
<ul class="doclist">
<li> A = mastery of all or almost all of the material
</li>
<li> B = good understanding of most of the material, perhaps with
a few gaps
</li>
<li> C = some understanding of most of the material, with
substantial gaps
</li>
<li> D = major gaps
</li>
<li> F = didn't show up / try
<div class="paragraph"> </div>
<div class="paragraph"> </div>
</li>
</ul>
</li>
<li> There is no pre-determined curve. We'd be perfectly delighted
to give everyone an A (for the exam, and for the course).
<ul class="doclist">
<li> Except: A+ grades will be given only for completing the
advanced track.
<div class="paragraph"> </div>
</li>
</ul>
</li>
<li> Standard and advanced exams will be graded relative to different
expectations (i.e., "the material" is different)
</li>
</ul>
<div class="paragraph"> </div>
<a name="lab360"></a><h3 class="section">Hints</h3>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> On each version of the exam, will be at least one problem taken
more or less verbatim from a homework assignment.
<div class="paragraph"> </div>
</li>
<li> On the advanced version, there will be an informal proof.
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab361"></a><h1 class="section">Expressions and Their Types</h1>
<div class="paragraph"> </div>
Thinking about well-typed expressions and their types is a great
way of reviewing many aspects of how Coq works...
<div class="paragraph"> </div>
<div class="paragraph"> </div>
(Discussion of Coq's view of the universe...) <br><br><br><br><br><br><br>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab362"></a><h1 class="section">Inductive Definitions</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab363"></a><h1 class="section">Tactics</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab364"></a><h1 class="section">Proof Objects</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab365"></a><h1 class="section">Functional Programming</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab366"></a><h1 class="section">Judging Propositions</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab367"></a><h1 class="section">More Type Checking</h1>
<div class="paragraph"> </div>
Good luck on the exam!
</div>
<div class="code code-tight">
<br/>
</div>
</div>
<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://www.lix.polytechnique.fr/coq/">coqdoc</a>
</div>
</div>
</body>
</html>