Themes in the lambda calculus and type theory

Fairouz Kamareddine

In this talk I treat three themes related to functions, types an d reductions. The first theme defends the use of low level functions as well as higher-order fuunctions and shows that in the presence of low-level functions a more accurate placing of Milner's ML and the Edinburgh LF can be given. Next, the approach to using class reduction rather than term reduction is proposed and this is followed by the approach of taking a single binder to represent type and term abstraction.