Is there any relation beetwen justification logic and type theory?

Question

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?

Answer 1

The evidence for a genuine relatedness is that the most influential inheritor of Russell's theory of types is Martin-Löf Type Theory which is also intrinsically connected to intuitionistic and constructive logic and mathematics.

Answer 2

The article quoted points out that justification logics were invented to:

provide constructive semantics to intuitionistic logic

And that

proofs are justifications in their purest forms

As a comment above points out this is reminiscent of the Curry-Howard Correspondance between types and propositions in intuitionistic logic.

This Correspondance shows that propositions in logic can be interpreted as a type; and where a type is inhabited, ie there is a term of that type, means that there is a proof for that proposition.

So, I would say yes.