Step-indexing

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).

References

The technique of step-indexing seems to have originated in the following paper.

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}
}

The name gas pattern famously occurs in the untyped lambda calculus chapter of the PLFA book:

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/},
}

The name fuel pattern occurs in the following paper:

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