NoDI seminar

Typed lambda calculi a la de Bruijn

Fairouz Kamareddine 15:00, April 15, 2014 G-610 New Main Building, Beihang University

Abstract: In this talk I discuss how N.G., de Bruijn influenced the development of lambda calculus and type theory. We know that de Bruijn was the first person to recommend dependent types which play a big role in theorem proving, we know that de Bruijn was the first to call for explicitly defining concepts in the lambda calculus (e.g., explicit definitions, explicit contexts, explicit substitutions) so that the theory and the implementation can be connected and hence it is easier to guarantee correctness and that specifications are met. De Bruijn also proposed a new way to write the lambda calculus that makes the lambda calculus and type theory much easier to work with. I will describe these recommendations of de Bruijn and explain how they helped in reaching new results in type theory and the foundations of programming language and mathematics.

Poster Slides Photos