Aarhus University Seal / Aarhus Universitets segl

Local Reasoning about a Copying Garbage Collector

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

Local Reasoning about a Copying Garbage Collector. / Torp-Smith, Noah; Birkedal, Lars; Reynolds, John C.

In: A C M Transactions on Programming Languages and Systems, Vol. 30, No. 4, 2008, p. 24-81.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

Torp-Smith, N, Birkedal, L & Reynolds, JC 2008, 'Local Reasoning about a Copying Garbage Collector', A C M Transactions on Programming Languages and Systems, vol. 30, no. 4, pp. 24-81.

APA

Torp-Smith, N., Birkedal, L., & Reynolds, J. C. (2008). Local Reasoning about a Copying Garbage Collector. A C M Transactions on Programming Languages and Systems, 30(4), 24-81.

CBE

Torp-Smith N, Birkedal L, Reynolds JC. 2008. Local Reasoning about a Copying Garbage Collector. A C M Transactions on Programming Languages and Systems. 30(4):24-81.

MLA

Torp-Smith, Noah, Lars Birkedal and John C. Reynolds. "Local Reasoning about a Copying Garbage Collector". A C M Transactions on Programming Languages and Systems. 2008, 30(4). 24-81.

Vancouver

Torp-Smith N, Birkedal L, Reynolds JC. Local Reasoning about a Copying Garbage Collector. A C M Transactions on Programming Languages and Systems. 2008;30(4):24-81.

Author

Torp-Smith, Noah ; Birkedal, Lars ; Reynolds, John C. / Local Reasoning about a Copying Garbage Collector. In: A C M Transactions on Programming Languages and Systems. 2008 ; Vol. 30, No. 4. pp. 24-81.

Bibtex

@article{a335bb385a37425f95562ff0cb22ac86,
title = "Local Reasoning about a Copying Garbage Collector",
abstract = "We present a programming language, model, and logic appropriate for implementing and reasoningabout a memory management system. We state semantically what is meant by correctness of acopying garbage collector, and employ a variant of the novel separation logics to formally specifypartial correctness of Cheney{\textquoteright}s copying garbage collector in our program logic. Finally, we provethat our implementation of Cheney{\textquoteright}s algorithm meets its specification using the logic we have givenand auxiliary variables. Udgivelsesdato: 2008",
author = "Noah Torp-Smith and Lars Birkedal and Reynolds, {John C.}",
note = "Paper id:: 10.1145/1377492.1377499",
year = "2008",
language = "English",
volume = "30",
pages = "24--81",
journal = "A C M Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery, Inc.",
number = "4",

}

RIS

TY - JOUR

T1 - Local Reasoning about a Copying Garbage Collector

AU - Torp-Smith, Noah

AU - Birkedal, Lars

AU - Reynolds, John C.

N1 - Paper id:: 10.1145/1377492.1377499

PY - 2008

Y1 - 2008

N2 - We present a programming language, model, and logic appropriate for implementing and reasoningabout a memory management system. We state semantically what is meant by correctness of acopying garbage collector, and employ a variant of the novel separation logics to formally specifypartial correctness of Cheney’s copying garbage collector in our program logic. Finally, we provethat our implementation of Cheney’s algorithm meets its specification using the logic we have givenand auxiliary variables. Udgivelsesdato: 2008

AB - We present a programming language, model, and logic appropriate for implementing and reasoningabout a memory management system. We state semantically what is meant by correctness of acopying garbage collector, and employ a variant of the novel separation logics to formally specifypartial correctness of Cheney’s copying garbage collector in our program logic. Finally, we provethat our implementation of Cheney’s algorithm meets its specification using the logic we have givenand auxiliary variables. Udgivelsesdato: 2008

M3 - Journal article

VL - 30

SP - 24

EP - 81

JO - A C M Transactions on Programming Languages and Systems

JF - A C M Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 4

ER -