A BRICS Mini-Course
April 29 and 30, 1998
Morten H. Sørensen
DIKU, University of Copenhagen, Denmark
This course presents some recent results about normalisation in lambda-calculus and type-theory. We aim to cover the theory of so-called perpetual reduction strategies (ie, reduction strategies that compute infinite reduction paths from lambda-terms) and techniques to infer strong normalisation (all reduction sequences from all terms eventually terminate) from weak normalisation (all terms have a reduction sequence to normal form) with an application to the so-called Barendregt-Geuvers-Klop conjecture about pure type systems.