One-year INRIA post-doctoral position

One-year INRIA post-doctoral position

[Frederic Blanqui]

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

Title: Generation of construction functions guaranteeing algebraic invariants
on concrete data types

Aim: Although concrete data types are very useful in defining complex data
structures, they are not always sufficient to adequately specify the data
structures required by some algorithms. Often, only a subset of the concrete
data type is in fact used since some invariants between the components are
mandatory to ensure the correctness of the program. Now, many invariants can be
described by using some equational theory. For instance, a sorted list is a
particular representative of the equivalence class of lists modulo
commutativity. The usual way to solve this problem is to use abstract data
types or, better, private data types if one does not want to lose the ability
of doing pattern matching. We propose to study the automatic generation of
certified construction functions guaranteeing algebraic invariants on concrete
data types, and develop an extension of OCaml with relational data types, that
is, data types with invariants described by user defined equations.

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=1155&nPostingTargetID=3197&option=52&sort=DESC&nDepartmentID=19

Competences and profile: The position involves research and development in the
area of functional programming, rewriting theory (in particular Knuth-Bendix
completion) and, possibly, interactive theorem proving (experience with a proof
assistant such as Coq is welcome). 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: Quotient (http://quotient.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.

Application deadline: 1st July 2007.

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

INRIA PhD position

[Frederic Blanqui]

Title: Generation of construction functions guaranteeing algebraic invariants
on concrete data types

Aim: Although concrete data types are very useful in defining complex data 
structures, they are not always sufficient to adequately specify the data 
structures required by some algorithms. Often, only a subset of the concrete 
data type is in fact used since some invariants between the components are 
mandatory to ensure the correctness of the program. Now, many invariants can 
be described by using some equational theory. For instance, a sorted list is a 
particular representative of the equivalence class of lists modulo 
commutativity. The usual way to solve this problem is to use abstract data 
types or, better, private data types if one does not want to lose the ability 
of doing pattern matching. We propose to study the automatic generation of 
certified construction functions guaranteeing algebraic invariants on concrete 
data types, and develop an extension of OCaml with relational data types, that 
is, data types with invariants described by user defined equations.

More information and online application on:
http://www.talentsplace.com/syndication1/inria/frdoc/details.html?id=PGTFK02620$

Competences and pro The position involves research and development in the
area of functional programming, rewriting theory (in particular Knuth-Bendix
completion) and 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/)
- project: Quotient (http://quotient.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.

Application deadline: 30 April 2007.

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

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