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

Mathematical logic seminar – Feb 27 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 II

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.