Step-indexing is a semantic technique for reasoning about programs with recursion, guarded recursion, or recursive types.
When used within proof assistants, step-indexing is also known as the gas pattern (see e.g. [Wadler, Kokke and Siek 2022] or the fuel pattern (see e.g. [Lennon-Bertrand et al. 2020]).
Appel, Andrew W., and David McAllester. 2001. ‘An Indexed Model of Recursive Types for Foundational Proof-Carrying Code’. ACM Transactions on Programming Languages and Systems 23 (5): 657–83. https://doi.org/10.1145/504709.504712.
@article{appel_2001,
title = {An indexed model of recursive types for foundational proof-carrying code},
volume = {23},
doi = {10.1145/504709.504712},
number = {5},
journal = {ACM Transactions on Programming Languages and Systems},
author = {Appel, Andrew W. and McAllester, David},
year = {2001},
pages = {657--683}
}
Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022.
@Book{plfa22.08,
author = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
title = {Programming Language Foundations in {A}gda},
year = {2022},
month = aug,
url = {https://plfa.inf.ed.ac.uk/20.08/},
}
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2022. Gradualizing the Calculus of Inductive Constructions. ACM Trans. Program. Lang. Syst. 44, 2, Article 7 (June 2022), 82 pages. https://doi.org/10.1145/3495528