Domain specific extensions and their framework

This topic is about extensions of Type Theory by a language modelled by the structure central to a specific application domain. The language provides a higher level of abstractions for reasoning with the type theoretic representation of the structure, encapsulating ``implementation details'' of the representation. We aim to have a unified framework for such an extension: an inherent, hierarchical description of the target structures independent of their possible representations, a method to derive a language for a given structure, and semantics that guarantees correct interaction between extensions and base systems. The framework is to lead to systematic machine implementations of extensions and further to a single, extensible system. For example, Szasz's theory of specifications can be seen as such an extension for the structure of specifications represented by (data type, predicate) pairs. Each natural step of inference in her theory (e.g., formation of higher-order specification) corresponds to several steps of inference on the pair-representations in the base Type Theory; so, the pairs models the theory. Note that representing the pairs by dependent sums and then manipulating them as plain types (e.g., applying function type formation) cannot give desired results. Similar developments can be expected for setoids , setoids with algebraic structure , domains , categories , etc.; study of various calculus encodings of objects , processes , etc., should also benefit from mixing machine-assisted reasoning at their original calculi level. Development of their theories will enjoy the usual advantages of modular programming; e.g., we can start experimenting with the use of new abstraction, even if its representation is not in place yet; we can change representation to support more abstractions without affecting a prior development.

For the framework, we will unify and extend the correspondences between various categorical structures and their internal languages, e.g., cartesian closed categories and simply typed lambda-calculi . We continue development and implementation of the framework for categories with extra structure based on universal properties . Compared to the more established one for categories with (essentially) algebraic structure , it gives rise to internal languages suited for more logical, rather than equational, reasoning with the familiar pattern of introduction and elimination rules. Further theoretical issues are: adaptation of sketches (e.g. ) for description of specific instances; generalisation to fibred categories for a clear semantics of interactions between the base and extensions; and iterations and other ways to combine extensions for a hierarchical, modular development of abstractions. The framework itself, which talks about Type Theory extensions, will be studied in the ordinary mathematical context, but constructive aspects in each instance, e.g. issues of equality, will be a part of investigation.


Last modified: Wed May 27 13:49:13 MET DST 1998