Charge! - A Framework for Higher-Order Separation Logic in Coq

Jesper Bengtson; Jonas B. Jensen; Lars Birkedal

doi:10.1007/978-3-642-32347-8_21

Charge! - A Framework for Higher-Order Separation Logic in Coq

Jesper Bengtson
, Jonas B. Jensen
, Lars Birkedal

Programming Logic and Semantics

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Original language	English
Title of host publication	Interactive Theorem Proving : Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
Publisher	Springer
Publication date	2012
Pages	315-331
ISBN (Print)	978-3-642-32346-1
ISBN (Electronic)	978-3-642-32347-8
DOIs	https://doi.org/10.1007/978-3-642-32347-8_21
Publication status	Published - 2012
Event	Interactive Theorem Proving - Princeton, New Jersey, Princeton, United States Duration: 13 Aug 2012 → 15 Aug 2012 Conference number: 3 http://itp2012.cs.princeton.edu/

Conference

Conference	Interactive Theorem Proving
Number	3
Location	Princeton, New Jersey
Country/Territory	United States
City	Princeton
Period	13/08/2012 → 15/08/2012
Internet address	http://itp2012.cs.princeton.edu/

Series	Lecture Notes in Computer Science
Volume	7406

Access to Document

10.1007/978-3-642-32347-8_21

http://link.springer.com/chapter/10.1007%2F978-3-642-32347-8_21

Cite this

@inproceedings{fa807e19f20448cdadd65e35677e7095,

title = "Charge! - A Framework for Higher-Order Separation Logic in Coq",

author = "Jesper Bengtson and Jensen, \{Jonas B.\} and Lars Birkedal",

year = "2012",

doi = "10.1007/978-3-642-32347-8\_21",

language = "English",

isbn = "978-3-642-32346-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "315--331",

booktitle = "Interactive Theorem Proving",

address = "Germany",

note = "Interactive Theorem Proving , ITP 2012 ; Conference date: 13-08-2012 Through 15-08-2012",

url = "http://itp2012.cs.princeton.edu/",

}

Bengtson, J, Jensen, JB & Birkedal, L 2012, Charge! - A Framework for Higher-Order Separation Logic in Coq. in Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Springer, Lecture Notes in Computer Science, vol. 7406, pp. 315-331, Interactive Theorem Proving , Princeton, United States, 13/08/2012. https://doi.org/10.1007/978-3-642-32347-8_21

Charge! - A Framework for Higher-Order Separation Logic in Coq. / Bengtson, Jesper; Jensen, Jonas B.; Birkedal, Lars.
Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Springer, 2012. p. 315-331 (Lecture Notes in Computer Science, Vol. 7406).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Charge! - A Framework for Higher-Order Separation Logic in Coq

AU - Bengtson, Jesper

AU - Jensen, Jonas B.

AU - Birkedal, Lars

N1 - Conference code: 3

PY - 2012

Y1 - 2012

U2 - 10.1007/978-3-642-32347-8_21

DO - 10.1007/978-3-642-32347-8_21

M3 - Article in proceedings

SN - 978-3-642-32346-1

T3 - Lecture Notes in Computer Science

SP - 315

EP - 331

BT - Interactive Theorem Proving

PB - Springer

T2 - Interactive Theorem Proving

Y2 - 13 August 2012 through 15 August 2012

ER -