Grothendieck Logical Relations.
The following paper (to be presented in TLCA'99) is available by anonymous FTP
or over the Web
Lambda Definability with Sums via Grothendieck Logical Relations
by Marcelo Fiore and Alex Simpson
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.
The paper is available over the Web:
or by anonymous FTP: