Talk "On formalizing lambda-definability and normalization-by-evaluation"

by Andreas Abel

Fri, 06 July 2018 at 11:10 am in Royal Holloway, United Kingdom

Abstract: Lambda-definability is concerned with the question: Given a (set-theoretic/mathematical) function, is there a lambda-term that implements this function? This question has been asked for untyped lambda calculus (computability) and typed lambda calculi. In the 1980s/90s Kripke models have been presented to characterize lambda-definability e.g. simply-typed lambda-calculus. It turned out that from a proof of lambda-definability one can extract a lambda-term in normal form. Thus, the computational content of lambda-definability is normalization-by-evaluation. In this talk, I will present lambda-definability for simple types and a formalization in Agda. It illustrates Kripke models and the connection between normalization and semantic completeness of the rules of intuitionistic propositional logic.