The semi-full closure of Pure Type Systems

被引：0
|
作者：
Barthe, G [1 ]
机构：
[1] Chalmers Tekn Hogskola, Inst Datavetenskap, Gothenburg, Sweden
[2] Univ Minho, Dept Informat, Braga, Portugal
来源：
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998 | 1998年 / 1450卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We show that every functional Pure Type System may be extended to a semi-full Pure Type System. Moreover, the extension is conservative and preserves weak normalization. Based on these results, we give a new, conceptually simple type-checking algorithm for functional Pure Type Systems.
引用
收藏
页码：316 / 325
页数：10
相关论文
共 50 条
  • [21] Pure type systems with explicit substitutions
    Fridlender, Daniel
    Pagano, Miguel
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2015, 25
  • [22] Syntactic analysis of η-expansions in Pure Type Systems
    Joachimski, F
    INFORMATION AND COMPUTATION, 2003, 182 (01) : 53 - 71
  • [23] Pure type systems with more liberal rules
    Bunder, M
    Dekkers, W
    JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (04) : 1561 - 1580
  • [24] Pure Type Systems with de Bruijn indices
    Kamareddine, F
    Ríos, A
    COMPUTER JOURNAL, 2002, 45 (02): : 187 - 201
  • [25] ARE THERE HILBERT-STYLE PURE TYPE SYSTEMS?
    Bunder, Martin W.
    Dekkers, Wil J. M.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2008, 4 (01)
  • [26] Pure type systems with subtyping (Extended abstract)
    Zwanenburg, J
    TYPED LAMBDA CALCULI AND APPLICATIONS, 1999, 1581 : 381 - 396
  • [27] Condensing lemmas for pure type systems with universes
    Jiménez, BCR
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1999, 1548 : 422 - 437
  • [28] Pure Type Systems without Explicit Contexts
    Geuvers, Herman
    Krebbers, Robbert
    McKinna, James
    Wiedijk, Freek
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (34): : 53 - 67
  • [29] SEMI-CLOSURE
    CROSSLEY, SG
    HILDEBRAND, SK
    TEXAS JOURNAL OF SCIENCE, 1971, 22 (2-3): : 99 - +
  • [30] CLOSURE OF MITTAG-LEFFLER-TYPE FUNCTION SYSTEMS
    DZHRBASHYAN, MM
    DOKLADY AKADEMII NAUK SSSR, 1974, 219 (06): : 1302 - 1305
12345