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 条
  • [41] Combined local semi-elliptical full-thickness skin graft for the closure of the free flap donor site
    Shimbo, Keisuke
    Okuhara, Yukako
    Yokota, Kazunori
    JOURNAL OF PLASTIC RECONSTRUCTIVE AND AESTHETIC SURGERY, 2019, 72 (11): : 1856 - 1857
  • [42] KAC TYPE MODELS OF SEMI-FINITE SPIN SYSTEMS
    COSTACHE, G
    PHYSICS LETTERS A, 1975, 54 (02) : 128 - 130
  • [43] CLOSURE SYSTEMS
    不详
    PACKAGE ENGINEERING, 1983, 28 (07): : 127 - &
  • [44] PURE LOGIC OF ITERATED FULL GROUND
    Lifland, Jon Erling
    REVIEW OF SYMBOLIC LOGIC, 2018, 11 (03): : 411 - 435
  • [45] ON POSITIONED ECO-GRAMMAR SYSTEMS AND PURE GRAMMARS OF TYPE 0
    Langer, Miroslav
    Kelemenova, Alica
    NEURAL NETWORK WORLD, 2013, 23 (02) : 81 - 91
  • [46] FUZZIFYING CLOSURE SYSTEMS AND CLOSURE OPERATORS
    Luo, X.
    Fang, J.
    IRANIAN JOURNAL OF FUZZY SYSTEMS, 2011, 8 (01): : 77 - 94
  • [47] Embedding pure type systems in the lambda-Pi-calculus modulo
    Cousineau, Denis
    Dowek, Gilles
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2007, 4583 : 102 - +
  • [48] Remarks on the equational theory of non-normalizing pure type systems
    Barthe, G
    Coquand, T
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2006, 16 (137-155) : 137 - 155
  • [49] Reviewing the classical and the de Bruijn notation for λ-calculus and pure type systems
    Kamareddine, F
    JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (03) : 363 - 394
  • [50] A first-order representation of pure type systems using superdeduction
    Burel, Guillaume
    TWENTY-THIRD ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2008, : 253 - 263
12345