Building Blocks for Step-Indexed Program Logics

Step-indexing and the later modality ▷ P are widely used in program logics. A key challenge in proofs in step-indexed logics is turning ▷ P into P, coined the later elimination problem. Later elimination cannot be done unconditionally, and has traditionally been linked one-to-one to the physical steps the program performs in the operational semantics. This one-to-one correspondence proved limiting in practice, and various techniques (flexible step-indexing and later credits) have been proposed to relax this correspondence.