# Characterisation of Approximation and (Head) Normalisation for $\lambda\mu$ using Strict Intersection Types

## TL;DR

This paper investigates the strict type assignment for lambda-mu calculus, introducing approximants to characterize head normalisation, normalisation, and strong normalisation through assignable types.

## Contribution

It defines approximants for lambda-mu-terms and establishes a semantics, providing new characterizations of normalisation properties via strict intersection types.

## Key findings

- Approximants generate a semantics for lambda-mu-terms.
- Typeability of an approximant matches the term's type.
- Characterizations for head normal form, normal form, and strong normalisation.

## Abstract

We study the strict type assignment for lambda-mu that is presented in [van Bakel'16]. We define a notion of approximants of lambda-mu-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable.