Sciweavers

ENTCS
2006
125views more  ENTCS 2006»
13 years 4 months ago
Formalizing Type Operations Using the "Image" Type Constructor
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...
Aleksey Nogin, Alexei Kopylov