Due June 2, 1999 before class

Part I

An important property of a typed language is "Type Soundness". Informally this property guarantees that no primitive operation of the language is ever applied to arguments of the wrong type. Find at least two popular languages with unsound type systems. Provide code that compiles without any warnings but produces a "type error" at runtime.

Part II

One of the reasons that type soundness is so important is that it has security implications. In the context of Java, show that an unsound type system could be exploited to violate the Java security model. Research published bugs in the type system that have caused security violations in the past.

Part III

Two tasks here:
  1. Consider the following simple type system for the lambda-calculus with constants (numbers, addition, etc). 
         (Syntax)

     E ::= x | C | (E E) | (lambda x.E)
     C ::= + | = | #t | #f | 0 | 1 | 2 | 3 | ...
     T ::= NAT | BOOL | T -> T

     CT = ([#t : BOOL], [#f : BOOL], [+ : NAT -> NAT -> NAT],
           [= : NAT -> NAT -> BOOL], [0 : NAT], [1 : NAT], [2 : NAT], ...)


     (Rules of Inference)

        GAMMA(x) = T     
     ------------------                     (Var)  
        GAMMA |- x:T     

        CT(C) = T   
     ----------------                       (Const)
      GAMMA |- C:T

           GAMMA, x:T |- E:T'
     -------------------------------        (Lam)
     GAMMA |- (lambda x.E) : T -> T'


     GAMMA |- E: T -> T' ,   GAMMA |- E':T
     -------------------------------------  (App)
             GAMMA |- (E E') : T'
    Show type derivations for the following expressions or argue that no type derivation exists: 
    
     *  ((= ((+ 1) 0)) 1)

     *  ((= #f) ((= 1) 0))

     *  ( (lambda f. (f 4)) (+ 3) )

     *  ( (lambda f. ( (+ (f 1)) (f #t) )) (lambda x. x) )

     *  ( (lambda x.(x x)) (lambda x.(x x)) )
    Example: A proof that 
        GAMMA |- ((lambda x.x) 3) : NAT
    would proceed along the following lines: 
        GAMMA, x:NAT (x) = NAT
    ---------------------- (Var)
    GAMMA, x:NAT |- x:NAT                           CT(3) = NAT
  ------------------------------------ (Lam)      --------------  (Const)
  GAMMA |- (lambda x. x) : NAT -> NAT             GAMMA |- 3:NAT
 ---------------------------------------------------------------  (App)
                   GAMMA |- ( (lambda x.x) 3 ) : NAT
  2. Add a constant Y as a recursion operator to the simply typed lambda calculus above. What's a reasonable type for the constant Y? How many types can you assign to the expression (Y (lambda x.x))?
Page visited times since November 18, 1996.

sabry@cs.uoregon.edu