EXTENSIONAL MODELS FOR POLYMORPHISM

被引：16

作者：

BREAZUTANNEN, V ^{[1
]}

COQUAND, T ^{[1
]}

机构：

[1] INST NATL RECH INFORMAT & AUTOMAT,F-78150 ROCQUENCOURT,FRANCE

来源：

THEORETICAL COMPUTER SCIENCE | 1988年 / 59卷 / 1-2期

关键词：

Computer Metatheory;

D O I：

10.1016/0304-3975(88)90097-7

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We present a general method for constructing extensional models for the Girard-Reynolds polymorphic lambda calculus - the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints like having only two polymorphic booleans and having only the numerals as polymorphic integers. Moreover, the method can be used to show that any simply typed lambda model can be fully and faithfully embedded into a model of the polymorphic lambda calculus.

引用

页码：85 / 114

页数：30

共 51 条

[21]

GORDON M, 1979, LECTURE NOTES COMPUT, V78

[22] LAMBDA-CALCULUS MODELS AND EXTENSIONALITY [J].

HINDLEY, R ;

LONGO, G .

ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1980, 26 (04) :289-310

[23]

HYLAND JME, 1987, UNPUB DISCRETE OBJEC

[24]

HYLAND JME, 1988, IN PRESS ANN PURE AP, V40

[25]

Kreisel G., 1959, CONSTRUCTIVITY MATH, P101

[26]

Leivant D., 1983, 24th Annual Symposium on Foundations of Computer Science, P460, DOI 10.1109/SFCS.1983.50

[27]

MATTHEWS DCJ, 1985, 63 U CAMBR COMP LAB

[28] WHAT IS A MODEL OF THE LAMBDA-CALCULUS [J].

MEYER, AR .

INFORMATION AND CONTROL, 1982, 52 (01) :87-122

[29]

MEYER AR, 1986, COMMUNICATION 0207

[30]

MEYER AR, 1987, 14TH P ACM S PRINC P, P253

← 1 2 3 4 5 6 →