BRICS · Contents · Programme

Normalisation in Lambda-Calculus and Type Theory

A BRICS Mini-Course
April 29 and 30, 1998

Lectures by
Morten H. Sørensen
DIKU, University of Copenhagen, Denmark

Course Contents

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