Rick Statman: Completeness of BCD for an operational semantics; forcing for proof theorists

Mathematical logic seminar – Feb 13 2018
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).

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.