Normalisation in lambda calculus and its relation to type inference
Paula G. Severi · TU/e Research Portal · 1996
This is an informal explanation of the main concepts and results of [Sev96]. We consider typed and untyped lambda calculi. For untyped lambda calculus, we give a new method to prove properties on normalisation. For typed lambda calculus, we study the meta-theory of pure type systems with definitions in detail and we give solutions for the problem of type inference in singly sorted pure type systems with definitions.