BRICS · Contents · Programme

**A BRICS Mini-Course**

**April 29 and 30, 1998**

**Lectures by
Morten H. Sørensen
**

**
**

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.

### Wednesday April 29, 1998, 15:15-17:00 in Auditorium D1

### Thursday April 30, 1998, 10:15-12:00 in Auditorium F

### Thursday April 30, 1998, 15:15-17:00 in Auditorium D3