CS 336 Homework

Homework 1

1. Exercises 3.5.13 and 3.5.14.
   

Homework 2

1. Write a detailed proof of Theorem 9.3.9.
2. Modify the simplebool program to add arithmetic terms and a second primitive type Nat.
   • Add Nat, 0, succ, pred iszero tokens to the lexer and parser (modifying the .lex and .grm files).
   • Extend the definition of terms in the parser (simplebool.grm) with arithemetic term forms (see tyarith/tyarith.grm).
   • Add type and term constructors to the abstract syntax (syntax.sml), and modify print functions accordingly (see tyarith/syntax.sml).
   • Modify the eval and typeof functions in core.sml to handle arithmetic terms.

Homework 3

1. Consider a Chan(T) type constructor (see Section 15.5), with operations

       newchan[T] : Unit -> Chan T
       send : Chan T * T -> Unit
       receive : Chan T -> T
   

   The send operation is similar to ":=", while receive is analagous to "!". Show why the Chan type constructor must be invariant, like Ref.
2. Exercise 16.2.1.
3. Prove 16.2.5.