[TYPES/announce] Postdoctoral position at King's College London: Higher order type theory for formal MDA

[Poernomo, Iman]

3 year postdoctoral research assistant position
The Predictable Assembly Laboratory
Department of Computer Science
Kingʼs College London

The Predictable Assembly Laboratory, lead by Iman Poernomo, is looking for a
postdoctoral research assistant to apply ideas from constructive program development
(the proofs-as-programs paradigm) to improve the trustworthiness of Model Driven
Architecture.

Model Driven Architecture (MDA) is a methodology based on the Meta Object Framework
(MOF) to develop software by means of successive refinements from abstract platformindependent
models to concrete platform-specific models. The purpose is to promote a
clear demarcation of abstract architecture and implementation-specific issues. Central to
MDA is the ability to define transformations as mappings between metamodels. Such
transformations are powerful, providing a systematic means of model refinement. They are
also dangerous: a single error in a transformation mapping can result in the systematic
introduction of a range of errors in a resulting model.

The purpose of this postdoctoral position is to explore ways of solving this problem through
formalisation of metamodels and model transformations within higher-order type theory.
The starting point for this approach is the observation that MDA transformations are
essentially higher-order programs, transforming types (metamodels) into types.
The postdoctoral position is funded by a large UK EPSRC grant awarded to Dr. Poernomo
at Kingʼs and Prof. John Derrick at the University of Sheffield to work on the topic of
“Higher-order refinement techniques for Model Driven Architecture”. The position will be
based in London with Dr. Poernomoʼs laboratory, but will involve close collaboration with
Prof. Derrickʼs team at Sheffield.

The candidate should hold, or be near to completing, a PhD in Computer Science with a
background in formal methods. Preferably the candidate should have a background in
higher-order type theory (for example, an understanding of the Calculus of Inductive
Constructions, Martin-Löf type theory, classical proofs-as-programs, logical frameworks, or
any of the Coq, ALF or Nuprl theorem provers). A background in the MOF, MDA or related
OMG standards would be helpful, but is not necessary.

The salary will be on grade 6: £33,784 (approximately 53,365USD or 41,335Euro) per
annum, inclusive of London allowance. There is an automatic annual increment of
approximately £1,343 and an annual pension contribution of £8,721.

For further information please contact Iman Poernomo at iman.poernomo at kcl.ac.uk