Grothendieck Logical Relations.

To: types@cis.upenn.edu
Subject: Grothendieck Logical Relations.
From: Marcelo Fiore <marcelo@cogs.susx.ac.uk>
Date: Thu, 7 Jan 1999 15:05:19 +0000 (GMT)

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:

    http://www.dcs.ed.ac.uk/~mf/TYPES/glr.dvi
    http://www.dcs.ed.ac.uk/~als/Research/glr.ps.gz

or by anonymous FTP:

    ftp://ftp.dcs.ed.ac.uk/pub/mf/TYPES/glr.dvi
    ftp://ftp.dcs.ed.ac.uk/pub/als/Research/glr.ps.gz