Lambda Calculus with Regular Types

被引：0
|
作者：
Dundua, Besik [1 ]
Florido, Mario [2 ]
Kutsia, Temur [3 ]
机构：
[1] Tbilisi State Univ, Inst Appl Math, Tbilisi, Georgia
[2] Univ Porto, Dept Comp Sci, Rua Campo Alegre 823, P-4100 Oporto, Portugal
[3] Johannes Kepler Univ Linz, Symbol Computat Res Inst, Linz, Austria
来源：
2015 17TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC) | 2016年
基金：
奥地利科学基金会;
关键词：
ALGOL; 60;
D O I：
10.1109/SYNASC.2015.29
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we introduce lambda(R) : a foundational calculus for sequence processing with regular expression types. Its term language is the lambda calculus extended with sequences of terms and its types are regular expressions over simple types. We provide a flexible notion of subtyping based on the semantic notion of nominal interpretation of a type. Then we prove that types are preserved by reduction (subject reduction), and that there exist no infinite reduction sequences starting at typed terms (strong normalization).
引用
收藏
页码：129 / 136
页数：8
相关论文
共 50 条
12345