Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Dependently typed records in type theory
Authors: Robert Pollack
Date: 2002
Publication Title:Formal Aspects of Computing
Publication Type:Journal Article Publication Status:Published
Volume No:13(3-5) Page Nos:386-402
The language \emph{Pebble} of Burstall and Lampson proposed dependent types as the underlying principle in a unified framework to explain facilities for programming in the large, such as \emph{modules} and \emph{signatures}, as well as for programming in the small. This proposal soon extended to large scale formal proof development as well. In fact, the functional approach to modularity has turned out to be a hard problem, which is still far from a fully satisfactory solution. This paper discusses aspects of this approach, including representations of records, informative signatures, sharing, and subtyping. My main contribution in this paper is to show that structures with dependent types and manifest fields (roughly ML style modules) are internally definable in a type theoretic framework extended with inductive-recursive definition. This shows that powerful modules follow from general principles without module-specific assumptions.
Links To Paper
No links available
Bibtex format
author = { Robert Pollack },
title = {Dependently typed records in type theory},
journal = {Formal Aspects of Computing},
publisher = {Springer},
year = 2002,
volume = {13(3-5)},
pages = {386-402},
doi = {10.1007/s001650200018},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh