[Prev][Next][Index][Thread]
Summary: A simple categorical model of predicative polymorphism
A week ago I asked for a *simple* categorical model of a predicatively
polymorphic
lambda calculus.
I received many responses, summarised below.
I especially looked for
W. Phoa: A simple categorical model of first-order polymorphism
Thomas Streicher pointed me to Hypatia. The paper isn't listed in the
bibliography but can be downloaded from
http://hypatia.dcs.qmw.ac.uk/data/P/PhoaWKS/poly.ps.Z
Now I have some reading to do.
Thank you very much to everyone who answered me,
Olaf
---------------------------------------------------------
From: "P. Scott" <scpsg@matrix.cc.uottawa.ca>
http://www.site.uottawa.ca/~phil/extra/papers/
One interesting reference characterizing lambda definability in
categorical models of core-ML is by Moez Alimohamed, TCS 146 (1995),
pp. 5-23. A general framework has been discussed by Mitchell and
Scedrov (in their paper "Notes on Sconing and Relators, SLNCS 702, 1993).
I don't know how "simple" you consider the following model, but one
approach to modelling core-ML is in a short paper by Girard, Scedrov, and
me: "Normal Forms and Cut-Free Proofs as Natural Transformations", in
Logic from Computer Science, ed. by Y. Moschovakis, Springer, 1992 (I
recommend you get the version from my account at Hypatia or my website,
since the original published one was badly printed by Springer (with
missing fonts)). This is related to Phil Wadler's work entitled "Theorems
for free". The general framework is discussed in the paper "Functorial
Polymorphism" by Bainbridge, Freyd, Scedrov, and me in TCS 70 (1990),
pp. 35-64.
---------------------------------------------------------
From: Daniel Leivant <leivant@cs.indiana.edu>
Norman Danner, who has just completed with me his PhD,
has an interesting chapter in his dissertation about
models of predicative polymorphism, albeit not
in a categorical style. I am responding here because
Norman is away from the net while moving to Los Angeles,
where he is taking a position at UCLA. I trust he will
respond to you in detail within a couple of weeks.
Norman has considered ordinal-stratified polymorphism,
a far more general formalism than first order polymorphism,
which can be construed as base level of the stratified
hierarchy.
---------------------------------------------------------
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
ein kategorieller Modellbegriff fuer praedikativ polymorphen lambda kalkuel
ist gegeben durch ``indexed cartesian closed categories over a category with
finite products''. Die Intuition ist, dass die indizierende Kategorie die der
Typkontexte und Substitutionen ist. In den Fasern lebt dann der Lambda Kalkuel
relativ zu einem fixierten Typkontext.
Eine eigentliche Literaturquelle zu diesem speziellen Thema faellt mir dazu
nicht ein. Wohl aber einige allgemeine Referenzen.
B. Jacobs Categorical logic and type theory (Elsevier 1999)
R. Croles Categories and Types
Herr Phoa hat tatsaechlich vor ein paar Jahren die Forschung verlassen.
Alerdings findet man seine Papiere noch via Hypatia.
da faellt mit noch eine referenz ein, die vielleicht am besten passt
873.68015 Alimohamed, Moez
A characterization of lambda definability in categorical models of
implicit polymorphism. (English)
Theor. Comput. Sci. 146, No.1-2, 5-23 (1995). MSC 1991: *68N15
---------------------------------------------------------
From: Solomon Feferman <sf@csli.Stanford.EDU>
This may not be relevant to your concerns, but I have a particular
axiomatic approach to predicative polymorphism that may be of
interest to you in connection with formulations of its principles.
You can find this in my paper "Polymorphic typed lambda-calculi in a
type-free axiomatic framework", in _Logic and Computation_ , Contemporary
Mathematics vol. 106, AMS Publications (1990), 101-136.
There is a follow-up paper with further refinements in "Logics for
termination and correctness of functional programs", in _Logic From
Computer Science_ (Y. N. Moschovakis, ed.) MSRI Pubs. vol.21, Springer
(1992), 95-127.