RECURSION OVER REALIZABILITY STRUCTURES

被引：27

作者：

AMADIO, RM

机构：

[1] Dipartimento di Informatica Corso Italia 40, I-56125, Pisa

来源：

INFORMATION AND COMPUTATION | 1991年 / 91卷 / 01期

关键词：

D O I：

10.1016/0890-5401(91)90074-C

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Realizability structures play a major role in the metamathematics of intuitionistic systems and they are a basic tool in the extraction of the computational content of constructive proofs. Besides their rich categorical structure and effectiveness properties provide a privileged mathematical setting for the semantics of data types of programming languages. In this paper we emphasize the modelling of recursive definitions of programs and types. A realizability model for a language including Girard's system F and an operator of recursion on types is given and some of its local properties are studied. © 1991.

引用

页码：55 / 85

页数：31

共 42 条

[1]

AMADIO R, 1988, 3RD IEEE LICS ED

[2]

AMADIO R, 1989, TR2889 U PIS

[3] METRIC INTERPRETATIONS OF INFINITE-TREES AND SEMANTICS OF NON DETERMINISTIC RECURSIVE-PROGRAMS [J].

ARNOLD, A ;

NIVAT, M .

THEORETICAL COMPUTER SCIENCE, 1980, 11 (02) :181-205

[4]

ASPERTI A, 1990, APPLIED CATEGORY THE

[5]

Banach S., 1922, FUND MATH, V3, P7

[6]

BARENDREGT HP, 1984, LAMBDA CALCULUS

[7]

BREAZUTANNEN V, 1988, THEORET COMPUT SCI, V59

[8]

BRUCE K, 1984, LECT NOTES COMPUT SC, V173

[9]

BRUCE K, 1988, 3RD IEEE LICS ED

[10]

CARBONI A, 1987, 3RD ACM S MATH FOUND

← 1 2 3 4 5 →