CMSC 221/321
Homework set 3
Due: Midnight, Tuesday, Oct 16, 2011

Reading: Lecture 5.

3.1: [25] Prove that SAEL[SSv] (small-step bind-by-value semantics for
SAEL) always terminates. You should be able to do this by modifying
your proof of termination for SAE[SS] in Homework 1.1.  (You can just
give the new parts of the proof that deal with the new language
features, i.e. let expressions.)

3.2: [25] Write an SML program that implements SAEL[BSn] (that is,
a big-step evaluator for SAEL with subst-by-name semantics).