\documentclass[a4paper]{article}
\usepackage{amssymb}
\pagestyle{empty}
\hoffset=-40pt
\voffset=-20pt
\textwidth 15.3cm
\textheight 22cm % to fit our printers

\begin{document}

\begin{center}{\huge The Superjump as a Type Constructor}\end{center}
\begin{center}{\large Dag Normann}\end{center}
\begin{center}{\large University of Oslo}\end{center}

\bigskip

Intuitionistic type theory represents the investigation of complex
set-theoretical constructions using constructive means.
A general philosophical question is how complex constructions and closure
principles we can grasp from an intuitionistic point of view. A special
case was discussed at a workshop in Uppsala in 1996:
Is it possible to grasp the Mahlo-property intuitionistically?

In this talk we will discuss the kind of type constructors needed in order
to obtain a structure of the same classical complexity as the first
recursively Mahlo ordinal. Harrington showed in 1972 that this ordinal
corresponds to the complexity of computations in the Superjump, a type 3
functional described by Gandy ten years earlier.
We will use typed structures of effective domains with totality to simulate
computations in the Superjump. Each application of the Superjump will
correspond to the application of a universe operator in type theory. The
technical result will be the match of the complexity of the constructed
typed structure and the computation theory of the superjump.

The construction will indicate which universes we must axiomatise to exist
in type theory in order to grasp the concept of Mahloness
intuitionistically from a type theory perspective.

\end{document}