-------------------------------------------------------------------------------
                                       
                                       
		   B O S T O N   U N I V E R S I T Y
                                       
		      Computer Science Department
                                       
			 P H D   D E F E N S E
                                       
			Friday December 22, 1995
                                       
				 3:00pm
                                       
			        MCS 135

-------------------------------------------------------------------------------
 
       Type Inference for System F with and without the Eta Rule
 
			       Joe Wells
 
  Church devised the lambda calculus intending it to be a foundation for
  mathematics instead of set theory, but the lambda calculus has been most
  useful as a model of computation.  Types have been added to the lambda
  calculus to enforce meaningful computations.  Girard and Reynolds
  independently invented the second-order polymorphically-typed lambda
  calculus, known as System F, to handle problems in logic and computer
  programming language design, respectively.  Viewing F in the "Curry
  style", associating types with untyped lambda terms, raises the
  questions of "typability" and "type checking".  Typability asks for a
  term whether there exists some type it can be given.  Type checking asks
  whether a term can be given a particular type.  The decidability of
  these problems has been settled for restrictions and extensions of F and
  related systems and complexity lower-bounds have been determined for
  typability in F, but decidability for F was an open question for many
  years.
  
  Subtyping relates types so that terms of one type automatically belong to
  other types.  Mitchell devised a simple subtyping system for F, one
  without bounded polymorphic quantification or a distinguished supertype of
  all types.  Mitchell showed extending F with his subtyping is the same as
  adding the eta rule to produce System F plus eta, which allows
  eta-equivalent terms to have the same types.  Until recently, the
  decidability of Mitchell's subtyping has been unknown as has been the
  decidability of type checking and typability for F plus eta.
  
  I discuss proofs of the undecidability of these problems:
  
    1. Type checking for F by a reduction from semi-unification.
  
    2. Typability for F by a reduction from type checking.
  
    3. Mitchell's subtyping system by a reduction from semi-unification,
       implying the undecidability of type checking for F plus eta.
  
    4. Typability for F plus eta by a reduction from type checking.
  
  These are the only proofs for 1, 2, and 4.  The proofs for 1 and 2 also
  work for the special case of the lambda-I calculus.  There is another
  proof for 3 which preceded my proof by a month, but which uses more
  complex and completely different methods.
  
Advisor: Prof. Assaf Kfoury
-------------------------------------------------------------------------------
For colloquium info, including directions, see http://cs-www.bu.edu/colloquium
   For more information contact Prof. Mark Crovella <crovella@bu.edu>
-------------------------------------------------------------------------------