In English

A family of universes for generic programming

Stevan Andjelkovic
Göteborg : Chalmers tekniska högskola, 2011. 87 s.
[Examensarbete på avancerad nivå]

Datatype-generic programming in the dependently typed setting can be achieved using the universe construction. The set of codes of the universe has an impact on the datatypes it can express and also on the set of supported datatype-generic functions.
For example a universe with a code for functions can express datatypes such as the Brouwer ordinals:
Oracle XML Developers Kit - Production XML-25011: Error processing XSLT stylesheet: ../index.xsl
file:////usr/local/tomcat/webapps/chex/local/xsl/output/html/normal/body.xsl<Line 340, Column 84>: XML-22021: (Error) Error parsing external document: 'Förbindelse vägras'.