• DocumentCode
    2023010
  • Title

    Semantics of separation-logic typing and higher-order frame rules

  • Author

    Birkedal, Lars ; Torp-Smith, Noah ; Yang, Hongseok

  • Author_Institution
    Copenhagen Univ., Denmark
  • fYear
    2005
  • fDate
    26-29 June 2005
  • Firstpage
    260
  • Lastpage
    269
  • Abstract
    We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning.
  • Keywords
    formal logic; inference mechanisms; reasoning about programs; type theory; coherent semantic; higher-order frame rules; local reasoning; separation-logic type; Computer languages; Genetic mutations; High level languages; Logic; Stress;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-2266-1
  • Type

    conf

  • DOI
    10.1109/LICS.2005.47
  • Filename
    1509230
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2023010