UCLA LOGIC COLLOQUIUM
                       Friday, November 19, 1999
                               4:00 p.m.
                       Mathematical Sciences 6627
                                 UCLA

                            NORMAN DANNER

                                (UCLA)

         "CAPTURING FUNCTION CLASSES WITH THE LAMBDA CALCULUS"

     One of the first results regarding Church’s untyped lambda
calculus is that, relative to an appropriate encoding of the natural
numbers, exactly the total recursive functions are representable.  Much
of the power of the untyped calculus arises from its (intentional)
failure to distinguish between function and argument (i.e., the same
term can be used in both capacities).  A typing discipline for the
lambda calculus reinstates this distinction, and when a typing
discipline is imposed, the collection of representable numeric
functions decreases dramatically.
     In this talk, I will survey some of the main typing disciplines
and their corresponding classes of representable functions.  I will
start with so-called simple typing, characterized by Schwichtenberg and
Statman in the late 60′s, and work through to some recent results of
Daniel Leivant and myself on systems of ramified polymorphism.

_________________________________________________________________________

                           http://www.math.ucla.edu/~hbe/logic.html