Speaker / Predavač : Prof. Pierre Lescanne
Title / Naslov: Explicit Substitutions and Intersection Types
Abstract / Rezime:
Substitution is the key mechanism of the evaluation of functions. Therefore, it is a key concept in lambda calculus. The calculus of explicit substitution is an extension of the lambda calculus which internalizes the process of substitution, allows a fine analysis of the way it works and provides abstract notions for the implementation of lambda calculus. Important questions are connected to termination yielding the famous question of the --preservation of strong normalization--, namely "Is a strongly normalizing term in the lambda calculus still strongly normalizing in the calculus of explicit substitution?". We address it through intersection types. In the talk we will start from basic notions, survey explicit substitution and present a type theory for characterizing strongly normalizing terms in the calculus of explicit substitution.