Justification logics, was introduced by Sergei Artemov, are epistemic logics which allow knowledge and belief modalities to be ‘unfolded’ into justification terms: instead of □X one writes t:X, and reads it as “X is justified by reason t”. Justification logic originated as part of a successful project to provide a constructive semantics for intuitionistic logic—justification terms abstracted away all but the most basic features of mathematical proofs.
The theory of types was introduced by Russell in order to cope with some contradictions he found in his account of set theory. In a system of type theory, each term has a type and operations are restricted to terms of a certain type. A typing judgment M:t describes that the term M has type t. For example, nat may be a type representing the natural numbers and 0, 1, 2, ... may be inhabitants of that type. The judgement that 2 has type nat is written as 2:nat.
It seems to me Artemov works in justification logic is similar to Russell works in type theory. Is there any evidence that there is a relation beetwen these two works?