CaltechTHESIS
  A Caltech Library Service

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.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:autoepistemic; knowledge reuse; logic; paraconsistent; semantics; software reuse
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Hickey, Jason J. (advisor)
  • Chandy, K. Mani (advisor)
Thesis Committee:
  • Hickey, Jason J. (chair)
  • Lea, Doug
  • Klavins, Eric
  • Chandy, K. Mani
Defense Date:10 May 2002
Non-Caltech Author Email:kiniry (AT) acm.org
Record Number:CaltechETD:etd-06062002-164914
Persistent URL:https://resolver.caltech.edu/CaltechETD:etd-06062002-164914
DOI:10.7907/TVTD-E826
ORCID:
AuthorORCID
Kiniry, Joseph Roland0000-0002-3589-2454
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:2468
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:07 Jun 2002
Last Modified:18 Dec 2020 01:16

Thesis Files

[img]
Preview
PDF (dissertation.pdf) - Final Version
See Usage Policy.

1MB

Repository Staff Only: item control page