\documentclass[12pt]{book}
\author{Peter Hancock}
\title{A title}
\date{Time-stamp: <1998-02-08 12:19:44 peter>}
\begin{document}
\tableofcontents
\chapter{Introduction}
\section{Overview, predigested summary of main points}
\section{Pointing out of original bits, and bits others contributed}
\section{Whatever is formally necessary}
\chapter{Apologia}
Argues for the interest of the subject matter,
which may be unusual in computer science.
\section{Functional programming languages with dependent type systems}
\section{Expressibility}
\section{Transition systems, simulations}
\section{Accessibility, transitivity}
\section{Concept of ordinal: ZF, type theory, etc}
\section{Ordinal notation systems, some examples}
Cantor normal form. Veblen-Sch\"utte hierarchy.
One using a `collapse' of the third (constructive)
number classes (basis of modern approach).
\section{Decidable type/proof checking, and recursion theoretic
reasons why decidability entails incompleteness}
\section{The `tide mark' of a type-system in an uncountable
domain: numerical functions, countable ordinals}
Numerical hierarchies: Hardy, Grzegorczyk, slow-growing.
\chapter{Basic arithmetic of transition systems}
Bread-and-butter.
\section{Arithmetic up to the exponential}
Some categorical descriptions. (As in Kahrs, towards a semantics for
termination proofs.)
\section{Ordinal exponentiation}
Why well-foundedness seems to be essential to develop
arithmetic beyond exponential.
\chapter{Models of type theory}
\section{Interest of predicativity}
The justification of inductive definitions.
Their `justification' by ${\Pi^1}_1$
impredicative quantification.
The (abandoned) idea of `meaning theory' based on
\emph{elimination} rules. Why it is not clear
why this idea was ever abandoned.
\section{General concept of model for dtt}
Martin-L\"of, Dybjer, Hofmann.
Martin-L\"of's pursuit of models that are locally formalisable.
\section{`Realisability ' models}
In which terms/programs are interpreted as `normal forms', plus
proofs that those normal terms are.
\section{Some examples: Aczel, Beeson?, Martin-L\"of/Caterina Coquand}
Martin-L\"of's pursuit of models that are locally formalisable.
\section{Wrinkles to get strong normalisation, and for `open' terms}
\section{Idea of this model}
Relativisation of realisability with respect to a new,
`indeterminate' type variable.
\section{The use of a universe operator to formalise positive
inductive definitions of sets, families of sets, etc}
$\mu$ for operators. Apparatus one needs: constructors,
structural recursion. Something about $\nu$.
\chapter{Execution of this model}
\chapter{Idea of lenses}
Note: the word `lens' will probably not occur.
A `lens' is a predicate transformer that can be used
to show a function preserves accessibility.
A `non-dependent' lens is one where the predicates are
`over a singleton' (degenerate) -- really they are
type-constructors.
\section{Non-dependent lenses}
How to use `arrow' and $\omega$-iteration to
simulate ordinals up to $\epsilon_0$.
\subsection{Iteration/Exponentiation and higher types}
\subsection{Iteration at transfinite types}
Aczel's solution. My solution. Inverse limits.
How the step to the `next universe' (extending and containing
a given one, closed under predicative $\Pi$) corresponds to
a `nesting' the Veblen function an extra level.
\chapter{Construction}
This is an exposition, extension and simplification of a
construction of ordinals up to $\Gamma_0$ done with
Anton Setzer. (Resurrecting my original idea.)
\chapter{Loose ends}
Upper bounds. Arithmetic combinators.
Exploitation of lenses to construct well-orderings in
the system modelled in the middle two chapters.
(Which probably has the same strength as type-theory with
the W-type, analysed by Setzer, using classical Kripke-Platek set theory
with one inaccessible and a few regulars beyond.)
Recent work on universes: Palmgren `super-universes' (closed under the
step to the next universe), Setzer,
Rathjen. The idea of forming universes in type theory is
to introduce them as (families of) sets closed under a specified
gaggle $\cal{G}$ of type-constructors. The universe then `reflects' $\cal{G}$.
Setzer's `Mahlo' universe.
The use of universes in functional programming. Translations of weak classical
systems into `classical' universes. (Coquand, Palmgren.)
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: