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 2002generated with PLT Scheme