EECS 762

Programming Language Foundation I


Homework 3

  1. Show how to formulate the evaluation rules for \(\lambda\)-terms in big-step style. (Pierce 5.3.8)
  2. The \(\lambda_\rightarrow\) with no base types is degenerate, in the sense that it has no well-typed terms at all. Why? (Pierce 9.2.1)
  3. Is there any context \(\Gamma\) of type \(T\) such that \(\Gamma\vdash x\ x:T\)? If so, provide \(\Gamma\) and \(T\) and show the typing derivation. If not, prove it. (Pierce 9.2.2, tricky)
  4. Do \(t\rightarrow t'\) and \(\Gamma\vdash t':T\) imply \(\Gamma\vdash t:T\)? (Pierce 9.3.10)
  5. Give typing and evaluation rules for wildcard abstractions and prove they can be derived from the derived form from class.