Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. In intuitionistic modal logic, boxes and diamonds are decoupled and not De Morgan dual. We propose justification counterparts to some intuitionistic modal logics by making diamonds explicit and introducing new terms called satisfiers. In this talk, we will hopefully introduce enough background information to eventually present an axiomatisation of these justification logics with a syntactic realisation procedure using cut-free (nested) sequent systems for intuitionistic modal logics.

(This is joint work with Paaras Padhiar, building up on other works with Anupam Das and with Roman Kuznets and Lutz Straßburger.)