[Prev][Next][Index][Thread]
Regarding "realizability, covers and sheaves, ..."
A few weeks ago, I made the following
two papers available by anonymous ftp.
Realizability, Covers, and Sheaves.
I. Applications to the Simply-Typed lambda-Calculus
II. Applications to the Second-Order Typed lambda-Calculus
Soon after, the following paper by J. M. E. Hyland and C.-H. L. Ong
was brought to my attention:
``Modified realizability topos and strong normalization proofs''
@INPROCEEDINGS{HylandOng
, AUTHOR = {Hyland, J. M. E. and Ong, C.-H. L.}
, TITLE = {Modified realizability topos and strong
normalization proofs}
, BOOKTITLE = {Typed Lambda Calculi and Applications}
, YEAR = {1993}
, EDITOR = {M Bezem and J.F. Groote}
, VOLUME = {664}
, SERIES = {Lecture Notes in Computer Science}
, PAGES = {179-194}
, PUBLISHER = {Springer Verlag}
}
The above paper by Hyland and Ong is definitely related to my two
papers, and it should have been referenced. Let me take this
opportunity to apologize for this omission.
Furthermore, I made a few (minor) corrections and additions.
Thus, I am sending this message to let people know that they
should get the newest version of these papers.
This also applies to my recent paper:
Kripke Models for the Second-Order lambda-Calculus
-- Jean
=======================================================================
N.B. There is no doubt that Hyland and Ong's approach and our approach
are related, but the technical details are very different,
and we are unable to make a precise comparison at this point.
What we can say is that our aim is not to provide
a new class of categorical models, but rather to provide
a better axiomatization of the conditions that make
proofs using reducibility go through. For this purpose, we believe that the
notion of a cover algebra (a special case of a Grothendieck topology)
is particularly well suited. We are also interested
in understanding how reducibility can be used to prove
other properties besides just SN, for example, confluence.
In fact, our results show that some aspects of proofs
using reducibility have very little to do with the SN property.
Clearly, further work is needed to clarify the connection
between Hyland and Ong's approach and ours.
To non-categorically inclined readers:
the only categories encountered in my papers are preorders.
Of course, this will be disapointing to categorically inclined readers!
================================================================
The file names for the above papers are
realiz1.dvi.Z
realiz2.dvi.Z
kripke1.dvi.Z
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 filename.dvi.Z
ftp> quit
Then, use the unix "uncompress" command on this file to
get the dvi file(s).