Summer school 2008:Exercises 1
Extend the Typed arithmetic expressions (value) language with binary pairs (see [http://www.cs.cmu.edu/~rwh/plbook/book.pdf PFPL Chapter 16] if you need a refresher on the syntax and typing rules for pairs).
This will be easiest if you start from Typed arithmetic expressions (value). Use the “Code: here” link in the top-left corner to download the code.
You will need to add:
- a type
prod T U - expression constructors for pairing
(pair E1 E2), and first and second projection(fst E)and(snd E). - new cases for evaluation
Get STELF to verify the totality of your extended evaluation judgement.
If you’re feeling ambitious, add disjoint sums ([http://www.cs.cmu.edu/~rwh/plbook/book.pdf PFPL Chapter 17]) as well! (solution)
Getting familiar with STELF
Section titled “Getting familiar with STELF”Read the discussion of STELF’s totality checker on this page so that you understand STELF’s error messages better.
Call-by-name
Section titled “Call-by-name”Do a call-by-name version of evaluation for Arithmetic expressions with let-binding. How would you prove evaluation terminates?