Summer school 2008:Exercises 1
|Summer school 2008|
Add pairs (solution)
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 Twelf to verify the totality of your extended evaluation judgement.
Getting familiar with Twelf
Read the discussion of Twelf's totality checker on this page so that you understand Twelf's error messages better.
Do a call-by-name version of evaluation for Arithmetic expressions with let-binding. How would you prove evaluation terminates?