Summer school 2008:Exercises 1

From The Twelf Project
Jump to: navigation, search
Summer school 2008

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:

  1. a type prod T U
  2. expression constructors for pairing (pair E1 E2), and first and second projection (fst E) and (snd E).
  3. 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)

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?