Beta-reduction as unification

Volume 46 / 1999

A. Kfoury Banach Center Publications 46 (1999), 137-158 DOI: 10.4064/-46-1-137-158


We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection types, and several of its basic properties.


  • A. Kfoury

Search for IMPAN publications

Query phrase too short. Type at least 4 characters.

Rewrite code from the image

Reload image

Reload image