|Time:|| 3:30pm - 4:30 pm
Wean Hall 8220
Department of Mathematical Sciences
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).