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 条

[1]

BOHM C, 1985, THEOR COMPUT SCI, V39, P135, DOI 10.1016/0304-3975(85)90135-5

[2]

Breazu-Tannen V., 1987, Proceedings of the Symposium on Logic in Computer Science (Cat. No.87CH2464-6), P7

[3]

BREAZUTANNEN V, 1987, LECT NOTES COMPUT SC, V250, P291

[4]

BREAZUTANNEN V, 1987, UNPUB PROOF CONJECTU

[5]

BREAZUTANNEN V, 1986, COMMUNICATION 0729

[6]

BREAZUTANNEN V, 1987, 14TH P S PRINC PROGR, P238

[7]

BREAZUTANNEN V, 1987, THESIS MIT

[8]

BRUCE KB, 1984, LECT NOTES COMPUT SC, V173, P131

[9]

BURSTALL RM, 1980, LISP C, P136

[10]

CARBONI A, 1988, LECT NOTES COMPUT SC, V298, P23

← 1 2 3 4 5 6 →