Sconing and Relators

To: types@uk.ac.gla.dcs, CATEGORIES@ca.mta
Subject: Sconing and Relators
From: andre@edu.upenn.cis.saul (Andre Scedrov)
Date: Tue, 17 Nov 92 17:39:31 EST
Approved: types@dcs.gla.ac.uk




                      NOTES ON SCONING AND RELATORS  

                     John Mitchell and Andre Scedrov


      ABSTRACT. A semantics of typed lambda calculi based on relations 
      is described. The main mathematical tool is a category-theoretic 
      method of sconing, also called glueing or Freyd covers.  Its 
      correspondence to logical relations is also examined. In the case 
      of polymorphic types, a central role is played by relators, i.e., 
      maps that take objects to objects and relations to relations.  
      Sconing may be used to express relators as functors, indeed, as 
      certain object maps on an appropriate category. These notes are 
      intended to be accessible to readers with minimal background in 
      category theory.  

  Available using anonymous ftp from host ftp.cis.upenn.edu and the file 
  pub/papers/scedrov/rel.dvi  or  pub/papers/scedrov/rel.ps .