Phase semantics (Girard 87) and its intuitionistic/noncommutative variants (Abrusci, Okada, Sambin, Troelstra, etc.) are provability semantics for linear logic and its variants. While they are sometimes considered "abstract nonsense" (or at least uninteresting from the viewpoint of computation), one cannot deny that it has a wide range of applications. For instance:

Undecidability (Lafont)
Decidability via finite model property (Lafont, Okada-Terui, Galatos-Jipsen)
Cut-elimination (Okada, Kanovitch-Okada-Scedrov, Belardinelli-Jipsen-Ono)
Denotational completeness (Girard, Streicher)
Conservativity (Kanovitch-Okada-Terui, Hamano-Takemura)
Criteria for cut-elimination (Terui, Ciabattoni-Terui)
Interpolation and amalgamation properties (Terui)
Polarity and Focalization

Thus phase semantics is a good tool for applications, and it is still useful to study it. In this talk, I will survey some uses of phase semantics and try to extract general patterns, hoping that it will lead to more applications and establishment of phase semantics as a solid, concrete and sensible tool.