When Is A Type Refinement An Inductive Type?
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Patricia Johann Ph.D, Professor (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
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 N-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 characterizations of refinements of inductive types, and argues that these characterizations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These characterizations 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.
When Is A Type Refinement An Inductive Type?
PDF (Portable Document Format)
206 KB
Created on 9/9/2016
Views: 380
Additional Information
- Publication
- Robert Atkey, Patricia Johann, and Neil Ghani (2011) "When Is A Type Refinement An Inductive Type?" . Proceedings, Foundations of Software Science and Computation Structures 2011 (FoSSaCS'11), pp. 72 - 87. Version Of Record Available From www.springer.com
- Language: English
- Date: 2011
- Keywords
- programming languages, vectors, semantic gap, VCons