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).