[Prev][Next][Index][Thread]
paper announcement
The preprint entitled :
From Computation to Foundations
via Functions and Application :
The Lambda-calculus and its Webbed Models.
Chantal Berline
is now available, either by clicking on the right place of my
www-page, which is located at :
http://www.logique.jussieu.fr/www.berline/index.html
or by ftp at :
ftp://ftp.logique.jussieu.fr/pub/distrib/berline/970522survey.dvi.gz
Paper copies (69 p.) are also available, just ask me at :
berline@logique.jussieu.fr
In a few words :
The paper is both : an introduction to lambda-calculus and its
motivations, aimed for mathematicians, and a survey of the diverse
classes of models of untyped lambda-calculus which can be described
from the structured set of their prime elements (the web). This covers
all classical models, many filter models, and all usual inverse limit
models, which appear as examples under this more tractable
presentation. Several applications of models are given, and we end
with a lot of open questions, including accessible (and even naive)
questions.
The paper also includes a sketchy presentation of Map Theory, which is
a common foundation for Mathematics, Logic and Computer Science based
on (untyped) lambda-calculus, and of its webbed models.
The paper issues from a talk given at a Conference on Modern Algebra
and its Applications. This, together with our personal interests,
explains why, except for the programming motivations connected with
the Curry-Howard isomorphism, we are mainly concerned here with
untyped lambda-calculus, and favour : its equational aspects, a simple
algebraic presentation of its models, and ... consistency
problems. However classical topics like the links between denotational
semantics (models) and operational semantics (computations) are also
treated.
Chantal Berline
berline@logique.jussieu.fr