Lambda Definability with Sums via Grothendieck Logical Relations

           Marcelo Fiore                     Alex Simpson

               COGS                  LFCS, Division of Informatics
        University of Sussex            University of Edinburgh 
      <marcelo@cogs.susx.ac.uk>       <Alex.Simpson@dcs.ed.ac.uk>


We introduce a notion of Grothendieck logical relation and use it to 
characterise the definability of morphisms in stable bicartesian closed
categories by terms of the simply-typed lambda calculus with finite
products and finite sums.  Our techniques are based on concepts from 
topos theory, however our exposition is elementary.