[TYPES/announce] INRIA PhD position

[Frederic Blanqui]

Title: Termination of higher-order rule-based programs

Application deadline: 30 April 2007.

Aim: Being able to prove that a program does not loop but eventually provides 
some result to the user is essential. Since termination is undecidable in 
general, various techniques and tools have been developed depending on the 
class of programs under consideration: rule-based, functional, logic or 
imperative programs. This subject aims at extending some procedure for checking 
the termination of simply-typed rule-based programs based on type checking and 
constraint solving to richer type disciplines, study its complexity, turn it 
into an automated termination prover by infering for each function a relation 
between the size of its arguments and the size of its result, and study its 
application to other class of programs.

More information and online application on:
http://www.talentsplace.com/syndication1/inria/frdoc/details.html?id=PGTFK026203F3VBQB6G68LONZ&LOV5=4509&LOV6=4514&LG=FR&Resultsperpage=20&nPostingID=1374&nPostingTargetID=3618&option=52&sort=DESC&nDepartmentID=28

Competences and profile: The position involves research and development in the 
area of lambda-calculus, rewriting, type systems, constraint solving (in 
particular Presburger arithmetic) and, possibly, interactive theorem proving. 
Speaking french is not necessary.

Salary: the monthly gross salary is approx. EUR 1,875.

Environment:
- laboratory: LORIA (http://www.loria.fr/)
- team: Protheo (http://protheo.loria.fr/)
- location: Nancy, in the East of France is at 1:30 from Paris by train, 1:30
from Luxembourg airport by car, and 1:30 from Germany and Belgium.

Contact: Frederic Blanqui (http://www.loria.fr/~blanqui/)

More information about INRIA PhD positions:
http://www.inria.fr/travailler/opportunites/doc.en.html