[Prev][Next][Index][Thread]
New paper available by ftp
The following paper is now available by anonymous ftp.
Comments are welcomed.
-- Jean Gallier
=============================================================
Kripke Models for the Second-Order lambda-Calculus
Abstract. We define a new class of Kripke structures
for the second-order lambda-calculus, and investigate the
soundness and completeness of some proof systems for
proving inequalities (rewrite rules) or equations.
The Kripke structures under consideration are equipped with
preorders that correspond to an abstract form of reduction,
and they are not necessarily extensional. A novelty of our approach
is that we define these structures directly as functors
A: W --> Preor equipped with certain natural
transformations corresponding to application and abstraction
(where W is a preorder, the set of worlds, and Preor
is the category of preorders).
We make use of an explicit construction of the exponential
of functors in the Cartesian-closed category Preor^{W}, and
we also define a kind of exponential depro{\Phi}{A}
to take care of type abstraction. We obtain soundness and completeness
theorems that generalize some results of Mitchell and Moggi to
the second-order lambda-calculus, and to sets of
inequalities (rewrite rules).
===============================================================
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 kripke1.dvi.Z
ftp> quit
Then, use the unix "uncompress" command on this file to
get the dvi file(s).