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.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=2023010
بازگشت