Home Teaching 3810 W '02 General Syllabus Readings Assignments Send Mail Read Mail

### Assignments

• Assignment 1: Exercises 1.15, 1.16, 1.17, and 1.18 of EoPL (pp.24-27) Please keep track of your type errors.
Due: Wed 23-1-2002. Brief class discussion of select exercises.
• Assignment 2: Define ! in ISWIM using Yv. Prove |- ! '3' =v '6' using the fixpoint theorem for Yv.
Due: Wed 23-1-2002. Brief class discussion.
• Assignment 3: Develop a module for finite functions. The module should support the following signature:
```   module type FF =
sig
type ('a,'b) F_F
val empty : ('a,'b) F_F
val extend : ('a,'b) F_F * 'a * 'b -> ('a,'b) F_F
val apply :  ('a,'b) F_F * 'a -> 'b
val domain : ('a,'b) F_F -> 'a list
end;;
```

Explain why you can't use plain functions to represent finite functions. Use functions from 'a to 'b to represent the functional aspect of the type F_F anyway.
Also see my Scheme implementation.
Due: Mon 4-2-2002. Brief class discussion.
• Assignment 4:
• Prove that fix! computes a fixpoint of functionals.
• Write a diverging program using SML's STLC core and exceptions. Explain why it is impossible to write this program in OCAML.
• Exhibit (or find) two CR rewriting systems on the same term set such that the combined systems are not CR.
• Design an extension of STLC with higher-order ref cells such that the language is SN. (No proof necessary.) Discuss whether it is a useful language.

• Assignment 5:
• Write a diverging program using SML's STLC core and exceptions. Explain why it is impossible to write this program in OCAML.
• Write a program in a language with subtyping and references such that something goes wrong at run-time, assuming the type system enforces the following rule only:
```			 sigma < tau
--------------------
tau ref < sigma ref
```
• Exhibit an infinitely ascending chain in Pierce's subtyping system. That is, define a series of types tau[i] such that
```		       for all i, tau[i] < tau[i+1]
```

 last updated on Thu Feb 28 17:51:52 EST 2002 generated with PLT Scheme