Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Universes for Generic Programs and Proofs in Dependent Type Theory
Universes for Generic Programs and Proofs in Dependent Type Theory
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 universes 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 a universe of codes for sets, and
generic formation, introduction, elimination, and equality
rules. However, here we consider several
smaller universes of interest for generic programming and universal
algebra. We thus formalize one-sorted and many-sorted term algebras,
as well as iterated, parameterized, generalized, and indexed
inductive definitions. We also show how to extend the techniques of
generic programming to these universes. Most of the definitions in
the paper have been implemented using the proof assistant Alfa for
dependent type theory.