The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

PhD place available

Due to a cancellation there is one PhD studentship available at the
Functional Programming Laboratory (http://fp.cs.nott.ac.uk/) on short
notice, that is the candidate would be required to start by January
2011. The studentship covers all fees and a standard maintainance
grant for 3 years.

The project is on "Higher Dimensional Type Theory", which is inspired
by the homotopy models of Type Theory, following a proposal by
Vladimir Voedowsky [1] and which is also related to recent results by
Garner & van den Berg [2] and Lumsdaine [3] on the weak omega groupoid
model of Type Theory. Our goal is to develop a syntactic theory, which
is computationally well behaved, which which supports higher
dimensional Identity Types (i.e. uniqueness of identity proofs doesn't
hold) and which supports extensional reasoning about functions.

We may be able to accomodate strong candidates with different
project ideas in related areas (Type Theory, Dependently Typed
Programming). If in doubt please contact me.

Please forward this information to students who may be interested in
it. Don't hesitate to contact me, if you are interested.

Cheers,
Thorsten Altenkirch

Reader in Computer Science
University of Nottingham

[1]
@article{voevodsky-equivalence,
  title={{The equivalence axiom and univalent models of type theory}},
  author={Voevodsky, V.},
  journal={Talk at CMU}
}
[2]
@conference{van2006types,
  title={{Types are weak $\omega$-groupoids}},
  author={van den Berg, B. and Garner, R.},
  booktitle={Workshop on “Identity Types—Topological and Categorical 
Structure”, Uppsala University},
  year={2006},
  organization={Citeseer}
}
[3]
@article{lumsdaine2009weak,
  title={{Weak $\omega$-categories from intensional type theory}},
  author={Lumsdaine, P.},
  journal={Typed Lambda Calculi and Applications},
  pages={172--187},
  year={2009},
  publisher={Springer}
}