A Type System for Higher-Order Intensional Logic Support for Variable Bindings in Hybrid Intensional-Imperative Programs in GIPSY

We present a type system theory for the General Intensional Programming System (GIPSY), a platform designed to support intensional programming languages (built upon higher-order intensional logic) and their imperative counter-parts for the eductive execution model. We extend the simple theory of types (STT) by adding the intensionality axiom to it. The intensionality principle covers language expressions that explicitly take into account a multidimensional context space of evaluation treating the context as a first-class value. We, therefore, describe and discuss the properties of such a type system and the related type theory. This work is done to complement our previous software engineering design and implementation study of the GIPSY type system.