Title.
Proof carrying formulas and reflexive combinatory logic.

Abstract.
Proof carrying formulas and the Logic of Proofs LP were invented in the 
1990s for solving a problem of the intended provability semantics of the 
modal and intuitionistic logic left open by Goedel. In this talk we will 
discuss possible applications of the Logic of Proofs in Computer 
Science. In the area of knowledge representation LP allows us to 
approach classical logical omniscience problem, which addresses a 
failure of the traditional logic of knowledge to distinguish between 
facts which are given, and the ones which can be only obtained after a 
long derivation process. The proof carrying formulas of LP naturally 
make this distinction. In the area of lambda-calculi and typed theories, 
proof carrying formulas bring in a much richer system of types capable 
of iterating the type assignment. We introduce and discuss the Reflexive 
Combinatory Logic (RCL) which provides a basic model of a programming 
language with a built-in compiler. 

Sergei Artemov, Graduate Center CUNY