The author introduces a nonstandard semantics for a conservative extension of the infinitary temporal programming logic of \textit{F. Kröger} [Acta Inf. 8, 243-266 (1977; Zbl 0347.68016)] and proves that the logic is sound and complete in the given semantics. He then develops a sequent calculus for this logic and proves that the calculus admits cut elimination and that the logic therefore has the subformula property. The sequent calculus involved has some connections with a calculus developed for program verification by \textit{H. Kawai} (unpublished) of the University of Osaka.