{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:00Z","timestamp":1775790720315,"version":"3.50.1"},"reference-count":35,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,6,7]],"date-time":"2011-06-07T00:00:00Z","timestamp":1307404800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Appel and McAllester's \"step-indexed\" logical relations have proven to be a\nsimple and effective technique for reasoning about programs in languages with\nsemantically interesting types, such as general recursive types and general\nreference types. However, proofs using step-indexed models typically involve\ntedious, error-prone, and proof-obscuring step-index arithmetic, so it is\nimportant to develop clean, high-level, equational proof principles that avoid\nmention of step indices. In this paper, we show how to reason about binary\nstep-indexed logical relations in an abstract and elegant way. Specifically, we\ndefine a logic LSLR, which is inspired by Plotkin and Abadi's logic for\nparametricity, but also supports recursively defined relations by means of the\nmodal \"later\" operator from Appel, Melli\\`es, Richards, and Vouillon's \"very\nmodal model\" paper. We encode in LSLR a logical relation for reasoning\nrelationally about programs in call-by-value System F extended with general\nrecursive types. Using this logical relation, we derive a set of useful rules\nwith which we can prove contextual equivalence and approximation results\nwithout counting steps.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:16)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":42,"title":["Logical Step-Indexed Logical Relations"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"given":"Derek","family":"Dreyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,6,7]]},"reference":[{"issue":"1-2","key":"10.2168\/LMCS-7(2:16)2011_Abadi:Cardelli:Curien:93","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1016\/0304-3975(93)90082-5","volume":"121","author":"Mart\u00edn Abadi, Luca Cardelli, and Pierre-","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(2:16)2011_abadi:fiore:lics96","unstructured":"Mart\u00edn Abadi and Marcelo P. Fiore. Syntactic considerations on recursive types. InLICS, 1996."},{"key":"10.2168\/LMCS-7(2:16)2011_acar-ahmed-blume-2008","doi-asserted-by":"crossref","unstructured":"Umut A. Acar, Amal Ahmed, and Matthias Blume. Imperative self-adjusting computation. InPOPL, 2008.","DOI":"10.1145\/1328438.1328476"},{"key":"10.2168\/LMCS-7(2:16)2011_ahmed-2006","doi-asserted-by":"crossref","unstructured":"Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. InESOP, 2006. Extennded\/corrected version available as Harvard University TR-01-06.","DOI":"10.1007\/11693024_6"},{"key":"10.2168\/LMCS-7(2:16)2011_adr-popl09","doi-asserted-by":"crossref","unstructured":"Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. InPOPL, 2009.","DOI":"10.1145\/1594834.1480925"},{"issue":"5","key":"10.2168\/LMCS-7(2:16)2011_appel-mcallester-2001","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"Andrew W. Appel and David McAllester","year":"2001","journal-title":"Transactions on Programming Languages and Systems"},{"key":"10.2168\/LMCS-7(2:16)2011_appel:vmm","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel, Paul-Andr\u00e9 Melli\u00e8s, Christopher D. Richards, and J\u00e9rome Vouillon. A very modal model of a modern, major, general type system. InPOPL, 2007.","DOI":"10.1145\/1190216.1190235"},{"key":"10.2168\/LMCS-7(2:16)2011_benton-hur09","doi-asserted-by":"crossref","unstructured":"Nick Benton and Chung-Kil Hur. Biorthogonality, step-indexing and compiler correctness. InICFP, 2009.","DOI":"10.1145\/1596550.1596567"},{"key":"10.2168\/LMCS-7(2:16)2011_BiermanGM:opeplp","doi-asserted-by":"crossref","unstructured":"Gavin Bierman, Andrew Pitts, and Claudio Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. InHOOTS, volume 41 ofENTCS, 2000.","DOI":"10.1016\/S1571-0661(04)80874-0"},{"key":"10.2168\/LMCS-7(2:16)2011_birkedal","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1006\/inco.1999.2828","volume":"155","author":"Lars Birkedal and Robert W. Harper","year":"1999","journal-title":"Information and Computation"},{"issue":"5:2","key":"10.2168\/LMCS-7(2:16)2011_BirkedalL:lapl-journal","first-page":"1","volume":"2","author":"Lars Birkedal, Rasmus E. M\u00f8gelberg, and","year":"2006","journal-title":"Logical Methods in Computer Science"},{"issue":"4","key":"10.2168\/LMCS-7(2:16)2011_brandt-henglein","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","volume":"33","author":"Michael Brandt and Fritz Henglein","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-7(2:16)2011_crary-harper-2007","doi-asserted-by":"crossref","unstructured":"Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. InComputation, Meaning and Logic: Articles dedicated to Gordon Plotkin. ENTCS, 2007.","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"10.2168\/LMCS-7(2:16)2011_dreyer+:lics09","doi-asserted-by":"crossref","unstructured":"Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical step-indexed logical relations. InLICS, 2009.","DOI":"10.1109\/LICS.2009.34"},{"key":"10.2168\/LMCS-7(2:16)2011_dreyer+:icfp10","doi-asserted-by":"crossref","unstructured":"Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. InICFP, 2010.","DOI":"10.1145\/1863543.1863566"},{"key":"10.2168\/LMCS-7(2:16)2011_dreyer+:popl10","doi-asserted-by":"crossref","unstructured":"Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. A relational modal logic for higher-order stateful ADTs. InPOPL, 2010.","DOI":"10.1145\/1706299.1706323"},{"key":"10.2168\/LMCS-7(2:16)2011_hur-dreyer11","unstructured":"Chung-Kil Hur and Derek Dreyer. A Kripke logical relation between ML and assembly. InPOPL, 2011."},{"issue":"1-2","key":"10.2168\/LMCS-7(2:16)2011_johann:voigtlaender","first-page":"63","volume":"69","author":"Patricia Johann and Janis Voigtl\u00e4nder","year":"2006","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-7(2:16)2011_Koutavas:Wand:06a","doi-asserted-by":"crossref","unstructured":"Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. InPOPL, 2006.","DOI":"10.1145\/1111037.1111050"},{"key":"10.2168\/LMCS-7(2:16)2011_Lassen-Levy:LICS2008","doi-asserted-by":"crossref","unstructured":"Soren B. Lassen and Paul B. Levy. Normal form bisimulation for parametric polymorphism. InLICS, 2008.","DOI":"10.1109\/LICS.2008.26"},{"key":"10.2168\/LMCS-7(2:16)2011_mason-talcott-91","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"Ian Mason and Carolyn Talcott","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-7(2:16)2011_mellies-vouillon","unstructured":"Paul-Andr\u00e9 Melli\u00e8s and J\u00e9rome Vouillon. Recursive polymorphic types and parametricity in an operational framework. InLICS, 2005."},{"key":"10.2168\/LMCS-7(2:16)2011_nakano-2000","unstructured":"Hiroshi Nakano. A modality for recursion. InLICS, 2000."},{"key":"10.2168\/LMCS-7(2:16)2011_neis+:icfp09","doi-asserted-by":"crossref","unstructured":"Georg Neis, Derek Dreyer, and Andreas Rossberg. Non-parametric parametricity. InICFP, 2009.","DOI":"10.1145\/1596550.1596572"},{"key":"10.2168\/LMCS-7(2:16)2011_pitts:parpoe","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129500003066","volume":"10","author":"A. M. Pitts","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.2168\/LMCS-7(2:16)2011_pitts:attapl","unstructured":"Andrew Pitts. Typed operational reasoning. In Benjamin C. Pierce, editor,Advanced Topics in Types and Programming Languages, chapter 7. MIT Press, 2005."},{"key":"10.2168\/LMCS-7(2:16)2011_pitts-reldom","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"Andrew M. Pitts","year":"1996","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-7(2:16)2011_Plotkin:85","unstructured":"Gordon D. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985."},{"key":"10.2168\/LMCS-7(2:16)2011_PlotkinGD:secotr","unstructured":"Gordon D. Plotkin. Second order type theory and recursion. Notes for a talk at the Scott Fest, February 1993."},{"key":"10.2168\/LMCS-7(2:16)2011_plotkin-abadi-93","unstructured":"Gordon D. Plotkin and Mart\u00edn Abadi. A logic for parametric polymorphism. InTLCA, 1993."},{"key":"10.2168\/LMCS-7(2:16)2011_sangiorgi-ea-2007","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. InLICS, 2007.","DOI":"10.1109\/LICS.2007.17"},{"key":"10.2168\/LMCS-7(2:16)2011_Stoevring-Lassen:POPL2007","doi-asserted-by":"crossref","unstructured":"Kristian St\u00f8vring and Soren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. InPOPL, 2007.","DOI":"10.7146\/brics.v14i4.21927"},{"key":"10.2168\/LMCS-7(2:16)2011_sumii:csl09","doi-asserted-by":"crossref","unstructured":"Eijiro Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. InCSL, 2009.","DOI":"10.1007\/978-3-642-04027-6_33"},{"issue":"5","key":"10.2168\/LMCS-7(2:16)2011_sumii-pierce-jacm","first-page":"1","volume":"54","author":"Eijiro Sumii and Benjamin Pierce","year":"2007","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-7(2:16)2011_Wadler:89","doi-asserted-by":"crossref","unstructured":"Philip Wadler. Theorems for free! InFPCA, 1989.","DOI":"10.1145\/99370.99404"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/698\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/698\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:06Z","timestamp":1681242846000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/698"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,7]]},"references-count":35,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:16)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1103.0510","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1103.0510","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6,7]]},"article-number":"698"}}