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