Part 1: Extending the language

The following language has been discussed in class:

Your job is to extend this language with a new construct, is-even e, that allows us to test whether an an expression evaluates to an even number or an odd number. You are allowed to assume basic mathematical judgments such as n is even or n is odd, as well as the fact that every number is even or odd and such facts of mathematics.

You need to give the following

• New rule(s) for the static semantics (typing rules)
• New rule(s) for the dynamic semantics (small-step evaluation rules)
• The extra case(s) of the progress theorem (prove them)
• The extra case(s) of the preservation theorem (prove them)
• The extra canonical forms/typing inversion lemmas, if any (do not prove them)

It is highly recommended that you email the TA with what you think the static and dynamic semantics are before you move on with the next parts of the assignment. You can do so with no penalty, and everyone will be happier if you get that correct before moving on.

You can download a partial proof of safety for the language without is-even in one of the following formats:

• PDF
• TeX
• SASyLF

Part 2: Constructive logic

Prove the following five statements. You may want to write these out on paper as opposed to LaTeX; feel free to use shorthand like A pr or pf A as shorthand for A proved.

(If that's too hard to read on the purple background)