[Prev][Next][Index][Thread]

New paper available by ftp


        Proving Properties of Typed \lambda-Terms
         Using Realizability, Covers, and Sheaves

                      Jean Gallier


This is a cleaned up version and merge of my previous two papers
"Realizablity, Covers and Sheaves, Part I and Part II".
I tried to simplify the presentation, and I have 
eliminated or relegated some secondary material to appendices. 
I hope that accomplished category theorists will not take
offense of my efforts to avoid more sophisticated aspects of
sheaves, in particular the connections with topos theory. 
On the other hand, I hope that these efforts will be helpful to
the novice.

-- Jean Gallier

File name: psheaf1.dvi.Z. 
To retrieve it, see end of message.
==================================================================

Abstract. We present a general method for proving properties of typed
\lambda-terms. This method is obtained by introducing a semantic
notion of realizability which uses the notion of a cover algebra (as
in abstract sheaf theory).  For this, we introduce a new class of
semantic structures equipped with preorders, called pre-applicative
structures.  These structures need not be extensional.  In this
framework, a general realizability theorem can be shown.  Kleene's
recursive realizability and a variant of Kreisel's modified
realizability both fit into this framework.  Applying this theorem to
the special case of the term model, yields a general theorem for
proving properties of typed \lambda-terms, in particular, strong
normalization and confluence.  This approach clarifies the
reducibility method by showing that the closure conditions on
candidates of reducibility can be viewed as sheaf conditions. The
above approach is applied to the simply-typed \lambda-calculus (with
types \rightarrow, \times, +, and \false), and to the second-order
(polymorphic) \lambda-calculus (with types \rightarrow and
\forall^{2}), for which it yields a new theorem.

==========================================================

The above paper(s) can be retrieved by anonymous ftp using the
instructions below.

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/gallier
ftp> binary
ftp> get  psheaf1.dvi.Z
ftp> quit

Then, use the unix "uncompress" command on this file to
get the dvi file(s).