Abstract
This seminar delved into Cohen's forcing technique and the analysis of its computational content covered in the seventh lecture. The speaker then explained realizability theory, a method of constructing models of logic formalizing and extending the BHK interpretation, and showed its formal links with forcing : realizability can be seen as non-commutative forcing. Pursuing this unification, he introduced the notion of implicational algebra, a structure that uniformly represents programs and types, realizers and logical formulas.
