Justification logic for intuitionistic modal logic.

Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic CK (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic IK and its extensions with the t and 4 axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.