Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2006-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2232/pdf |
| _version_ | 1797268749205635072 |
|---|---|
| author | Lars Birkedal Noah Torp-Smith Hongseok Yang |
| author_facet | Lars Birkedal Noah Torp-Smith Hongseok Yang |
| author_sort | Lars Birkedal |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:37:25Z |
| format | Article |
| id | doaj.art-2b2dd234b7dc452ea492cae879775aa7 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:25Z |
| publishDate | 2006-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-2b2dd234b7dc452ea492cae879775aa72024-03-08T08:39:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742006-11-01Volume 2, Issue 510.2168/LMCS-2(5:1)20062232Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like LanguagesLars BirkedalNoah Torp-SmithHongseok YangWe 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.https://lmcs.episciences.org/2232/pdfcomputer science - logic in computer sciencef.3d.3 |
| spellingShingle | Lars Birkedal Noah Torp-Smith Hongseok Yang Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages Logical Methods in Computer Science computer science - logic in computer science f.3 d.3 |
| title | Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
| title_full | Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
| title_fullStr | Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
| title_full_unstemmed | Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
| title_short | Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
| title_sort | semantics of separation logic typing and higher order frame rules for algol like languages |
| topic | computer science - logic in computer science f.3 d.3 |
| url | https://lmcs.episciences.org/2232/pdf |
| work_keys_str_mv | AT larsbirkedal semanticsofseparationlogictypingandhigherorderframerulesforalgollikelanguages AT noahtorpsmith semanticsofseparationlogictypingandhigherorderframerulesforalgollikelanguages AT hongseokyang semanticsofseparationlogictypingandhigherorderframerulesforalgollikelanguages |