Type-level Computation Using Narrowing in Ωmega

AbstractΩmega is an experimental system that combines features of both a programming language and a logical reasoning system. Ωmega is a language with an infinite hierarchy of computational levels. Terms at one level are classified (or typed) by terms at the next higher level. In this paper we report on using two different computational mechanisms. At the value level, computation is performed by reduction, and is largely unconstrained. At all higher levels, computation is performed by narrowing