Back to my publications
Aleksey Nogin and Alexei Kopylov.
Formalizing type operations using the “Image” type
constructor.
In Proceedings of the 13th Workshop on Logic, Language,
Information and Computation (WoLLIC 2006), volume 165 of Electronic
Notes in Theoretical Computer Science, pages 121–132. Elsevier,
2006.
Extended version was submitted to Information and Computation
Journal.
ENTCS
Entry,
PDF.
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper we introduce a notion of an “image” of a given type under a mapping that captures the spirit of many of such semantical arguments. This allows us to use the new “image” type to formalize within the type theory a large range of type constructors that were traditionally formalized via postulated axioms.We demonstrate the ability of the “image” constructor to express “forgetful” types by using it to formalize the “squash” and “set” type constructors. We also demonstrate its ability to handle types with non-trivial equality relations by using it to formalize the union type operator. We demonstrate the ability of the “image” constructor to express certain inductive types by showing how the type of lists and a higher-order abstract syntax type can be naturally formalized using the new type constructor.
The work presented in this paper have been implemented in the MetaPRL proof assistant and all the derivations checked by MetaPRL.
Last update: Saturday, January 27, 2007 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)