Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

When is a type refinement an inductive type

Atkey, Robert and Johann, Patricia and Ghani, Neil (2011) When is a type refinement an inductive type. [Proceedings Paper]

Full text not available in this repository. (Request a copy from the Strathclyde author)

Abstract

Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the ℕ-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purpose-specific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.

Item type: Proceedings Paper
ID code: 32474
Keywords: programming language, typed programming, data types, Electronic computers. Computer science, Computer Science(all)
Subjects: Science > Mathematics > Electronic computers. Computer science
Department: Faculty of Science > Computer and Information Sciences
Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 09 Aug 2011 16:46
    Last modified: 28 Mar 2014 06:10
    URI: http://strathprints.strath.ac.uk/id/eprint/32474

    Actions (login required)

    View Item