Blog

- Show how to formulate the evaluation rules for \(\lambda\)-terms in big-step style. (Pierce 5.3.8)
- 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)
- 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)
- Do \(t\rightarrow t'\) and \(\Gamma\vdash t':T\) imply \(\Gamma\vdash t:T\)? (Pierce 9.3.10)
- Give typing and evaluation rules for wildcard abstractions and prove they can be derived from the derived form from class.

Maintained by Perry Alexander

Hosted on GitHub Pages

Theme by orderedlist