[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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.poern...@kcl.ac.uk

Reply via email to