[Agda] PhD place at the FP lab, Nottingham

[Thorsten Altenkirch]

PhD place available

A PhD position in the Functional Programming Laboratory (FP Lab) at
the University of Edinburgh starting January 2011 is available. The
studentship is for 3 years, it covers the university fees for EU
nationals and a contains a standard mainatainance grant. The starting
date is not negotiable.

Work at the FP lab (http://fp.cs.nott.ac.uk/) covers functional
programming, its applications and theory including dependently typed
programming, constructive type theory and applications of category
theory. The FP lab currently comprises 4 academic staff, 2 research
assistants, and 9 PhD students and provides a thriving research
environment through regular meetings, seminars and visitors.

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 foundations of Intuitionistic Type Theory, in
particular addressig the question wether equality of types can be
isomorphism or a related notion. Such a "Higher Dimensional Type
Thoery" would make it easy to reason about matehmatical concepts upto
isomorphism. This is inspired by 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,
Categorical Logic). If in doubt please contact me.

Please let me know before 5 November 2010, wether you are interested,
and tell me about yourself and your background. If possible include a
CV. 

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}
}