A While-Rule in Martin-Löf's Theory of Types. - Roland Carl Backhouse; A. Khamiss (Comput. J., 1987)