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.=20 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=3D{{The equivalence axiom and univalent models of type theory}}, author=3D{Voevodsky, V.}, journal=3D{Talk at CMU} } [2] @conference{van2006types, title=3D{{Types are weak $\omega$-groupoids}}, author=3D{van den Berg, B. and Garner, R.}, booktitle=3D{Workshop on =93Identity Types=97Topological and = Categorical Structure=94, Uppsala University}, year=3D{2006}, organization=3D{Citeseer} } [3] @article{lumsdaine2009weak, title=3D{{Weak $\omega$-categories from intensional type theory}}, author=3D{Lumsdaine, P.}, journal=3D{Typed Lambda Calculi and Applications}, pages=3D{172--187}, year=3D{2009}, publisher=3D{Springer} } [For admin and other information see: http://www.mta.ca/~cat-dist/ ]