Kind Theory

Citation

Kiniry, Joseph Roland (2002) Kind Theory. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/TVTD-E826. https://resolver.caltech.edu/CaltechETD:etd-06062002-164914

Abstract

My contribution, described in this thesis, is a theory that is meant to assist in the construction of complex software systems. I propose a notion of structure that is independent of language, formalism, or problem domain. I call this new abstraction a kind, and its related formal system, kind theory. I define a type system that models the structural aspects of kind theory. I also define an algebra that models this type system and provides a logic in which one can specify and execute computations.

A reflective definition of kind theory is reviewed. This reflective specification depends upon a basic ontology for mathematics. By specifying the theory in itself, I provide an example of how one can use kind theory to reason about reuse in general formal systems.

I provide examples of the use of kind theory in reasoning about software constructs in several domains of software engineering. I also discuss a set of software tools that I have constructed that realize or use kind theory.

A logical framework is used to specify a type theoretic and algebraic model for the theory. Using this basic theorem prover one can reason about software systems using kind theory. Also, I have constructed a reuse repository that supports online collaboration, houses software assets, helps search for components that match specifications, and more. This repository is designed to use kind theory (via the logical framework) for the representation of, and reasoning about, software assets.

Finally, I propose a set of language-independent specification constructs called semantic properties which have a semantics specified in kind theory. I show several uses of these constructs, all of which center on reasoning about reusable component-based software, by giving examples of how these constructs are applied to programming and specification languages. I discuss how the availability of these constructs and the associated theory impact the software development process.

Thesis Files