Justification logic and type theory as formalizations of intuitionistic propositional logic.

We explore two ways of formalizing Kreisel's addendum to the Brouwer–Heyting–Kolmogorov interpretation. To do this, we compare Artemov's justification logic with simply typed |$\lambda $| calculus. First, we provide a completeness result for Kripke style semantics of the implicational fragment of the intuitionistic logic of proofs. Then we introduce a map from justification terms into |$\lambda $| terms, which can be viewed as a method of extracting the computational content of the justification terms. Then we examine the interpretation of Kreisel's addendum in justification logic along with the image of the resulting justification terms under our map. [ABSTRACT FROM AUTHOR]