A typed semantics of higher-order store and subtyping

被引：0
|
作者：
Schwinghammer, J [1 ]
机构：
[1] Univ Sussex, Brighton, E Sussex, England
来源：
THEORETICAL COMPUTER SCIENCE, PROCEEDINGS | 2005年 / 3701卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We consider a call-by-value language, with higher-order functions, records, references to values of arbitrary type, and subtyping. We adapt an intrinsic denotational model for a similar language based on a possible-world semantics, recently given by Levy [14], and relate it to an untyped model by a logical relation. Following the methodology of Reynolds [22], this relation is used to establish coherence of the typed semantics, with a coercion interpretation of subtyping. We obtain a typed denotational semantics of (imperative) object-based languages.
引用
收藏
页码：390 / 405
页数：16
相关论文
共 50 条
  • [1] Typed operational semantics for higher-order subtyping
    Compagnoni, A
    Goguen, H
    [J]. INFORMATION AND COMPUTATION, 2003, 184 (02) : 242 - 297
  • [2] Initial Semantics for higher-order typed syntax in Coq
    Ahrens, Benedikt
    Zsido, Julianna
    [J]. JOURNAL OF FORMALIZED REASONING, 2011, 4 (01): : 25 - 69
  • [3] HIGHER-ORDER SUBTYPING
    STEFFEN, M
    PIERCE, B
    [J]. PROGRAMMING CONCEPTS, METHODS AND CALCULI, 1994, 56 : 511 - 530
  • [4] Higher-order subtyping
    Pierce, B
    Steffen, M
    [J]. THEORETICAL COMPUTER SCIENCE, 1997, 176 (1-2) : 235 - 282
  • [5] Predicate transformer semantics of a higher-order imperative language with record subtyping
    Naumann, DA
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2001, 41 (01) : 1 - 51
  • [6] Typed higher-order narrowing without higher-order strategies
    Antoy, S
    Tolmach, A
    [J]. FUNCTIONAL AND LOGIC PROGRAMMING, PROCEEDINGS, 1999, 1722 : 335 - 352
  • [7] Relational Semantics for Effect-Based Program Transformations: Higher-Order Store
    Benton, Nick
    Kennedy, Andrew
    Beringer, Lennart
    Hofmann, Martin
    [J]. PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 301 - 311
  • [8] Syntactic Metatheory of Higher-Order Subtyping
    Abel, Andreas
    Rodriguez, Dulma
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2008, 5213 : 446 - 460
  • [9] Higher-order subtyping and its decidability
    Compagnoni, A
    [J]. INFORMATION AND COMPUTATION, 2004, 191 (01) : 41 - 103
  • [10] Foundations for the implementation of higher-order subtyping
    Crary, K
    [J]. ACM SIGPLAN NOTICES, 1997, 32 (08) : 125 - 135
12345