Semantics of Separation-Logic Typing and Higher-Order Frame Rules

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Lars Birkedal Articles by Noah Torp-Smith Articles by Hongseok Yang

20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)

Chicago, Illinois

June 26-June 29

ISBN: 0-7695-2266-1

	ASCII Text	x
	Lars Birkedal, Noah Torp-Smith, Hongseok Yang, "Semantics of Separation-Logic Typing and Higher-Order Frame Rules," Logic in Computer Science, Symposium on, pp. 260-269, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005.

	BibTex	x
	@article{ 10.1109/LICS.2005.47, author = {Lars Birkedal and Noah Torp-Smith and Hongseok Yang}, title = {Semantics of Separation-Logic Typing and Higher-Order Frame Rules}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2005}, issn = {1043-6871}, pages = {260-269}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2005.47}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Logic in Computer Science, Symposium on TI - Semantics of Separation-Logic Typing and Higher-Order Frame Rules SN - 1043-6871 SP260 EP269 A1 - Lars Birkedal, A1 - Noah Torp-Smith, A1 - Hongseok Yang, PY - 2005 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER -

Lars Birkedal, IT University of Copenhagen

Noah Torp-Smith, IT University of Copenhagen

Hongseok Yang, Seoul National University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2005.47

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.

Citation:

Lars Birkedal, Noah Torp-Smith, Hongseok Yang, "Semantics of Separation-Logic Typing and Higher-Order Frame Rules," lics, pp.260-269, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.