Aarhus University Seal / Aarhus Universitets segl

Logical Step-Indexed Logical Relations

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

Standard

Logical Step-Indexed Logical Relations. / Dreyer, Derek; Ahmed, Amal; Birkedal, Lars.

In: Logical Methods in Computer Science, Vol. 7, No. 2:16, 2011.

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

Harvard

Dreyer, D, Ahmed, A & Birkedal, L 2011, 'Logical Step-Indexed Logical Relations', Logical Methods in Computer Science, vol. 7, no. 2:16. https://doi.org/10.2168/LMCS-7(2:16)2011

APA

Dreyer, D., Ahmed, A., & Birkedal, L. (2011). Logical Step-Indexed Logical Relations. Logical Methods in Computer Science, 7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

CBE

Dreyer D, Ahmed A, Birkedal L. 2011. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science. 7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

MLA

Dreyer, Derek, Amal Ahmed, and Lars Birkedal. "Logical Step-Indexed Logical Relations". Logical Methods in Computer Science. 2011. 7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

Vancouver

Dreyer D, Ahmed A, Birkedal L. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science. 2011;7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

Author

Dreyer, Derek ; Ahmed, Amal ; Birkedal, Lars. / Logical Step-Indexed Logical Relations. In: Logical Methods in Computer Science. 2011 ; Vol. 7, No. 2:16.

Bibtex

@inproceedings{e0bf33b47f3343e3afd211635ae55fc4,
title = "Logical Step-Indexed Logical Relations",
abstract = "Appel and McAllester's {"}step-indexed{"} logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal {"}later{"} operator from Appel, Melli`es, Richards, and Vouillon's {"}very modal model{"} paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.",
author = "Derek Dreyer and Amal Ahmed and Lars Birkedal",
year = "2011",
doi = "10.2168/LMCS-7(2:16)2011",
language = "English",
volume = "7",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "International Federation for Computational Logic",
number = "2:16",

}

RIS

TY - GEN

T1 - Logical Step-Indexed Logical Relations

AU - Dreyer, Derek

AU - Ahmed, Amal

AU - Birkedal, Lars

PY - 2011

Y1 - 2011

N2 - Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel, Melli`es, Richards, and Vouillon's "very modal model" paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.

AB - Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel, Melli`es, Richards, and Vouillon's "very modal model" paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.

U2 - 10.2168/LMCS-7(2:16)2011

DO - 10.2168/LMCS-7(2:16)2011

M3 - Conference article

VL - 7

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2:16

ER -