Exercise set 7

For this week, we will take a look at the imperative programming language IMP. In particular, we will be working with the stuff discussed in chapter 2 of FSoPL. Recall the grammar:

a ::= n | X | a_0 + a_1 | a_0 - a_1 | a_0 x a_1

b ::= true | false | a_0 = a_1 | a_0 <= a_1 | ~b | b_0 /\ b_1 | b_0 \/ b_1

c ::= skip | X := a | c_0; c_1 | if b then c_0 else _1 | while b do c

The operational semantics of IMP can be found in sections 2.2, 2.3, and 2.4.

After reading the chapter (and convincing yourself that it makes sense), try to solve the following exercises:

• Exercises 2.3 and 2.4 in FSoPL
• Exercise 2.7 in FSoPL
• Consider the parallels between natural deduction in propositional logic and the operational semantics of IMP. What do the systems have in common, and how do they differ?

Looking ahead: You can, if time allows, try to solve exercise 2.1 from AF lecture notes (i.e. prove Theorem 2.6 in the notes).

Next week, we will learn a bit more about induction and the principles of metatheorems.