Picture water droplets

Developing mathematical theories of the physical world: Open Access research on fluid dynamics from Strathclyde

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Mathematics & Statistics, where continuum mechanics and industrial mathematics is a specialism. Such research seeks to understand fluid dynamics, among many other related areas such as liquid crystals and droplet evaporation.

The Department of Mathematics & Statistics also demonstrates expertise in population modelling & epidemiology, stochastic analysis, applied analysis and scientific computing. Access world leading mathematical and statistical Open Access research!

Explore all Strathclyde Open Access research...

Refining inductive types

Atkey, Robert and Johann, Patricia and Ghani, Neil (2012) Refining inductive types. Logical Methods in Computer Science, 8 (2). ISSN 1860-5974

[img] PDF
1205.2492.pdf
Preprint
License: Creative Commons Attribution-NonCommercial 4.0 logo

Download (387kB)

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 must often store redundant information about data and their refinements. In this paper we show how to generically derive inductive characterisations of refinements of inductive types, and argue that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. Our 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.