Nominal essential intersection types

被引：0

作者：

Ayala-Rincon, Mauricio ^{[1
]}

Fernandez, Maribel ^{[2
]}

Rocha-Oliveira, Ana Cristina ^{[1
]}

Ventura, Daniel Lima ^{[3
]}

机构：

[1] Univ Brasilia, Dept Ciencia Comp & Matemat, Brasilia, DF, Brazil

[2] Kings Coll London, Dept Informat, London, England

[3] Univ Fed Goias, Inst Informat, Goiania, Go, Brazil

来源：

THEORETICAL COMPUTER SCIENCE | 2018年 / 737卷

关键词：

Nominal syntax; Nominal rewriting; Binding; Essential intersection types; Subject reduction; NORMALIZATION; COMPLETENESS; UNIFICATION; SEMANTICS;

D O I：

10.1016/j.tcs.2018.05.008

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Nominal systems are an alternative approach for the treatment of variables in computational systems, where first-order syntax is generalised to provide support for the specification of binding operators. In this work, an intersection type system is presented for nominal terms. The subject reduction property is shown to hold for a specialised notion of typed nominal rewriting, thus ensuring preservation of types under computational execution. (C) 2018 Elsevier B.V. All rights reserved.

引用

页码：62 / 80

页数：19

共 50 条

[31] Intersection types for explicit substitutions
Lengrand, S
Lescanne, P
Dougherty, D
Dezani-Ciancaglini, M
van Bakel, S
INFORMATION AND COMPUTATION, 2004, 189 (01) : 17 - 42
[32] Intersection Types for Unboundedness Problems
Parys, Pawel
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (293): : 7 - 27
[33] Simple SubTypes of Intersection Types
Statman, Rick
FUNDAMENTA INFORMATICAE, 2019, 170 (1-3) : 307 - 324
[34] STRONG CONJUNCTION AND INTERSECTION TYPES
ALESSI, F
BARBANERA, F
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 520 : 64 - 73
[35] Intersection types and computational effects
Davies, R
Pfenning, F
ACM SIGPLAN NOTICES, 2000, 35 (09) : 198 - 208
[36] Isomorphism of intersection and union types
Coppo, Mario
Dezani-Ciancaglini, Mariangiola
Margaria, Ines
Zacchi, Maddalena
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2017, 27 (05) : 603 - 625
[37] ESSENTIAL EXTENSIONS AND INTERSECTION THEOREMS
SCHELTER, W
PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 1975, 53 (02) : 328 - 330
[38] Judgmental subtyping systems with intersection types and modal types
Seo, Jeongbong
Park, Sungwoo
ACTA INFORMATICA, 2013, 50 (7-8) : 359 - 380
[39] Judgmental subtyping systems with intersection types and modal types
Jeongbong Seo
Sungwoo Park
Acta Informatica, 2013, 50 : 359 - 380
[40] Action and event, two distinct nominal types?
Haas, Pauline
Grea, Philippe
LANGUE FRANCAISE, 2015, (185): : 85 - +

← 1 2 3 4 5 →