Summer school 2008:Exercises 1
From The Twelf Project
| Summer school 2008 |
[edit] Add pairs (solution)
Extend the Typed arithmetic expressions (value) language with binary pairs (see 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 Twelf to verify the totality of your extended evaluation judgement.
If you're feeling ambitious, add disjoint sums (PFPL Chapter 17) as well! (solution)
[edit] Getting familiar with Twelf
Read the discussion of Twelf's totality checker on this page so that you understand Twelf's error messages better.
[edit] Call-by-name
Do a call-by-name version of evaluation for Arithmetic expressions with let-binding. How would you prove evaluation terminates?
