Sergei Artemov
(Graduate Center CUNY)

"Justified Knowledge"

Plato's classical definition specifies knowledge as "justified true belief." The traditional, Hintikka-style modal logic approach to knowledge has not captured the "justification" component, which has remained a focus of attention in the mainstream epistemology. A recent progress in proof theory revealed a basic structure of justification and allowed us to augment the classical model to capture all components of the tripartite knowledge definition. This led to a new notion of "justified knowledge", which provided a fresh look at the common knowledge phenomenon as well as at the classical logical omniscience problem. Corresponding formal systems find applications well beyond the area of their origin. In lambda-calculi and typed theories, this creates a new rich system of self-referential types. In the context of typed programming languages this leads to a theory of data types containing programs. It also gives a theoretically clean schema of building tactic-based verification systems.

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc. and Netlogic, Inc.