AH%MIT-MC@sri-unix.UUCP (07/19/84)
From: Arline H. Benford <AH @ MIT-MC>
[Forwarded from the MIT bboard by Laws@SRI-AI.]
DATE: Tuesday, July 24, 1984
TIME: 1:45PM Refreshments
2:00PM Lecture
PLACE: NE43-512A
"THE SEMANTICS OF EXPLICIT POLYMORPHISM"
Kim B. Bruce
Department of Mathematical Sciences
Williams College
Williamstown, MA
Facilities for defining GENERIC or POLYMORPHIC routines, i.e., routines which
can have several typed instantiations, are now available in programming
languages such as Ada, Clu, and ML. We consider a typed calculus called
second-order polymorphic lambda calculus as a theoretical model for
EXPLICIT polymorphism -- where types appear as parameters of procedures as in
Ada and Clu (and as opposed to ML).
The proof theory of the second-order polymorphic lambda calculus was reasonably
well understood before there was much concern over its semantics (as is common
in the development of logical systems). The problem with assigning semantics
to the system is that terms may be applicable to their own types, which
involves a classical type violation. Reynolds attempted to construct a kind of
set-theoretic model for the language but ran into difficulties, and
subsequently demonstrated that no such model is possible. Donahue
attempted to construct a model using complete lattices and also failed.
Finally, McCracken and also Haynes successfully constructed models usng Scott
domains.
We describe in this talk a general notion of model for the second-order lambda
calculus. In support of our definitions we establish soundness and
completeness results relative to our semantics for the previously given axiom
system for the calculus. We also review related results and open problems.
HOST: Professor Albert R. Meyer