[Prev][Next][Index][Thread]
Sconing and Relators
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 .