Universes for Generic Programs and Proofs in Dependent Type Theory
Marcin Benke and
Peter Dybjer and
Patrik Jansson
Paper entry in Chalmers publication library (CPL) and full text available from the ACM library.
Abstract
We show how to write generic programs and proofs in Martin-Löf type
theory. To this end we consider several extensions of Martin-Löf's
logical framework for dependent types. Each extension has a universe
of codes (signatures) for inductively defined sets with generic
formation, introduction, elimination, and equality rules. These
extensions are modeled on Dybjer and Setzer's finitely axiomatized
theories of inductive-recursive definitions, which also have
universes of codes for sets, and generic formation, introduction,
elimination, and equality rules. Here we consider several smaller
universes of interest for generic programming and universal
algebra. We formalize one-sorted and many-sorted term algebras, as
well as iterated, generalized, parameterized, and indexed inductive
definitions. We also show how to extend the techniques of generic
programming to these universes. Furthermore, we give generic proofs
of reflexivity and substitutivity of a generic equality test. Most of
the definitions in the paper have been implemented using the proof
assistant Alfa for dependent type theory.
The Alfa code
is available in the subdirectory Code/.
BibTeX entry for this paper:
@article{benkedybjerjansson2003:gendepty,
author = {Marcin Benke and Peter Dybjer and Patrik Jansson},
title = {Universes for Generic Programs and Proofs in
Dependent Type Theory},
volume = 10,
number = 4,
year = 2003,
issn = {1236-6064},
pages = {265--289},
publisher = {Publishing Association Nordic Journal of Computing},
address = {Finland}
}
BibTeX entries for all the references.