[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Applications are invited for a postdoctoral position at INRIA Grenoble, France. The appointment will be in the areas of programming languages, computational logic, and program analysis and verification. The selected candidate will be expected to conduct research on some of the following topics: * the design of logics for reasoning about programs manipulating tree-shaped structures * the implementation of satisfiability solvers for such logics, and * the use of the implemented systems in building type-checkers and reasoners for actual programs. The WAM project seeks to establish logical foundations and automated reasoning techniques with applications concerning, but not limited to, static analysis of programs manipulating XML documents, pointer and heap analysis, program verification. Information about previous relevant research is available online: http://wam.inrialpes.fr/web-solver/webinterface.html The position is under the supervision of Nabil Layaida (INRIA) and Pierre Geneves (CNRS). Applicants should have interests in programming languages, type theory, and/or mathematical logic, with a concern in the intersection of theory and practice. Expertise in the following areas are particularly welcomed: - program analysis - formal methods - automated reasoning The fellowship is offered for a period of up to 16 months and can start as early as October 2009. A prerequisite for employment is a doctoral degree in Computer Science or closely related field. Applications should include: - detailed curriculum vitae, in pdf format - copies of relevant publications, or url-pointers to them - the names of at least 2 referees - a statement outlining the applicant's suitability to the project. Applications should be sent to Nabil Layaida <nabil.laya...@inria.fr> and Pierre Geneves <pierre.gene...@.inria.fr>. Informal enquiries about the position are welcomed.