Time:  3:30pm  4:30 pm 
Room: 
Wean Hall 8220

Speaker: 
Rick Statman Department of Mathematical Sciences CMU 
Title: 
Completeness of BCD for an operational semantics;
forcing for proof theorists

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