Intuitionistic S4 as a logic of topological spaces

We design and study various topological semantics for the diamond-free intuitionistic modal logic iS4, an intuitionistic analogue of S4. Ultimately we prove that ordinary topological spaces can be used as semantics, using the specialization order to interpret intuitionistic implication and the interior for the modality. Some of our soundness and completeness results are mechanised in Coq.