The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

A one-year INRIA post-doctoral position is available:

Title: Certifying the termination of programs

Application deadline: 15 April 2007 on
http://www.talentsplace.com/syndication1/inria/frpostdoc/details.html?id=PGTFK026203F3VBQB6G68LONZ&LOV5=4508&LOV6=4514&LG=FR&Resultsperpage=20&nPostingID=1183&nPostingTargetID=3228&option=52&sort=DESC&nDepartmentID=19

Aim: Checking that a program does not loop but eventually gives some answer to 
the user is an important property. To answer this problem, undecidable in 
general, many techniques and tools have been developed these last years. Since 
these techniques are becoming more complex and applied on larger examples, it 
becomes difficult to guarantee the correctness of their implementations. The 
CoLoR project aims at providing a platform for automatically certifying the 
termination of programs, in particular those in rule-based programming 
languages. The idea is to provide to termination provers like TPA, AproVE, 
CiME, etc. a common format for termination proof skeletons from which full 
formal proofs can be automatically generated and checked. For full formal 
proofs, the powerful proof assistant and checker Coq has been chosen. Thanks to 
the contributions of various people, the CoLoR project already provides an 
important Coq library of termination criteria. We also began to develop a 
grammar for termination proof skeletons (XML Schema) and a program, called 
Rainbow, that generates and checks in Coq the correctness of termination proof 
skeletons expressible in this grammar. Currently, Rainbow only handle 
polynomial interpretations. It is however sufficient for certifying 19.3% of 
the problems of the database of the annual international competition on 
termination. So, the main objectives of this postdoc is to extend this embryo 
of termination proof grammar and develop the Rainbow program further in order 
to handle the other termination techniques of the CoLoR library. This requires 
to develop algorithms for automatically checking the conditions of application 
of these termination criteria and implement them in the Coq tactic language 
Ltac. This will probably require various adaptations and extensions of the 
CoLoR library. The complexity of the algorithms will depend on the amount of 
information provided by the grammar. Finding a good granularity for the grammar 
is therefore very important.

More information and online application on:
http://www.talentsplace.com/syndication1/inria/frpostdoc/details.html?id=PGTFK026203F3VBQB6G68LONZ&LOV5=4508&LOV6=4514&LG=FR&Resultsperpage=20&nPostingID=1183&nPostingTargetID=3228&option=52&sort=DESC&nDepartmentID=19

Competences and profile: The position involves research and development on 
termination of rewrite systems and automated theorem proving. Knowledge of a 
functional programming language like OCaml and a proof assistant like Coq is 
required. Speaking french is not necessary.

Requirements: Candidates are required to hold a PhD degree between May 2006 and 
June 2007.

Salary: the monthly gross salary is approx. EUR 2,150.

Environment:
- laboratory: LORIA (http://www.loria.fr/)
- team: Protheo (http://protheo.loria.fr/)
- project: CoLoR (http://color.loria.fr/)
- location: Nancy, in the East of France is at 1:30 from Paris by tren, 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 post-doctoral positions:
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html