  The importance of intuitionistic temporal logics in Computer Science and
Artificial Intelligence has become increasingly clear in the last few years.
From the proof-theory point of view, intuitionistic temporal logics have made
it possible to extend functional languages with new features via type theory,
while from its semantical perspective several logics for reasoning about
dynamical systems and several semantics for logic programming have their roots
in this framework. In this paper we consider several axiomatic systems for
intuitionistic linear temporal logic and show that each of these systems is
sound for a class of structures based either on Kripke frames or on dynamic
topological systems. Our topological semantics features a new interpretation
for the `henceforth' modality that is a natural intuitionistic variant of the
classical one. Using the soundness results, we show that the seven logics
obtained from the axiomatic systems are distinct.
