Mathematical logic seminar – Feb 13 2018
Time: 3:30pm – 4:30 pm
Room: Wean Hall 8220
Speaker: Rick Statman
Department of Mathematical Sciences
Title: Completeness of BCD for an operational semantics; forcing for proof theorists
Intersection types provide a type discipline for untyped λ-calculus. The formal theory for assigning intersection types to lambda terms is BCD (Barendregt, Coppo, and Dezani). We show that BCD is complete for a natural operational semantics. The proof uses a primitive forcing construction based on Beth models (similar to Kripke models).