Sergei Artemov, New York.
Explicit knowledge representation in logic and computer science

Abstact:
Since the early the 1930ies the Brouwer-Heyting-Kolmogorov (BHK)
informal provability semantics has been generally recognized as the 
intended semantics for intuitionistic logic. It took quite a long time  to
find its formal model. First Goedel built an embedding of
intuitionistic logic into the classical modal logic S4 based on the 
intuition of the latter as the logic of classical provability. Then 
Goedel suggested using the original BHK format of proof carrying
formulas to build a provability model for S4, hence for intuitionistic 
logic as well. This Goedel's program was completed in the mid 1990s in 
the Logic of Proofs (LP) which was able to realize the whole of S4 and 
hence provide a desired provability semantics for S4 as well as for 
intuitionistic propositional logic.

The Logic of Proofs turned out to be a general purpose calculus of 
evidence which finds its applications well beyond the area of its  origin.
In lambda-calculi and typed theories, LP brings in a much richer  system
of types capable of iterating the type assignment, in particular, 
self-referential types. In the context of typed programming languages 
this leads to a theory of data types containing programs. In the area of 
formal epistemology the Logic of Proofs helps formalizing a notion of 
justification and hence capturing in full Plato's tripartite definition 
of knowledge as justified true belief. This leads to a new notion of 
justified knowledge which provides a fresh look at the common knowledge 
phenomenon as well as at the classical logical omniscience problem. The 
latter addresses a failure of the traditional logic of knowledge to 
distinguish between given facts, like logical axioms on one hand, and 
knowledge which can be only obtained after a long computation. The proof 
carrying formulas of LP naturally make this distinction.