[Prev][Next][Index][Thread]
Paper on beta-eta-complete model of system F
We announce a new paper, proving that there is a Scott domain model of
system F which is beta-eta complete (= its equational theory is
beta-eta).
The paper is avaible on the home pages of the authors, Chantal Berline
(main page) and Stefano Berardi (clic on the "Technical report" item)
The proof generalizes Friedman argument for beta-eta completeness of the
full model of simply typed lambda calculus. Friedman argument is merged
with Plotkin's logical relation method to produce the desired proof.
The model proved to be beta-eta complete is itself of interest, being
obtained by combining two Scott's information systems, one for
modelizing terms, the other one for modelizing types, together with a
compatibility condition.
Chantal Berline
Stefano Berardi