L7

Question 1

In what sense is SysF explicit?

Answer 1

176-177

Question 2

How does type inference work?

Answer 2

178

Question 3

What are effects?

Answer 3

179-182

Question 4

What is state?

Answer 4

183

Question 5

Give a type system for state

Answer 5

184

Question 6

Give opsem for StateLan

Answer 6

185-186

Question 7

Give term typing rules in StateLan

Answer 7

187-188

Question 8

Strategy for proving type safety in StateLan

Answer 8

189

Question 9

Store and configuration typing rules in StateLan

Answer 9

190

Question 10

Which naively stated safety theorem is broken?

Answer 10

191

Question 11

Store extension

Answer 11

192

Question 12

Substitution and structural properties of StateLan

Answer 12

193

Question 13

Progress for StateLan

Answer 13

194

Question 14

Preservation for StateLan

Answer 14

195

Question 15

Why state reduces ability to statically analyse

Answer 15

196-197

Question 16

Landin’s knot

Answer 16

198

Question 17

Why is termination no longer a theorem

Answer 17

199

Question 18

Explain whether we have to choose between state/effects and logical consistency

Answer 18

200

Question 19

1. Using Landin’s knot, implement the fibonacci function.

Answer 19

201

Question 20

2. The type safety proof for state would fail if we added a C-like free() operation to the reference API.
3. 1 Give a plausible-looking typing rule and operational semantics for free.
4. 2 Find an example of a program that would break.

Answer 20

202