This paper analyses the computational behaviour of ?- term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating).
Citation:
Makoto Tatsuta, Mariangiola Dezani-Ciancaglini, "Normalisation is Insensible to \lambda-Term Identity or Difference," lics, pp.327-338, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006