A postdoctoral position is available at INRIA Rhône-Alpes to contribute to the field of interoperability on the semantic web and more especially the use of proof techniques for certifying knowledge transformations.
The worldwide web is both the main factor and the first application of digital information interchange. The semantic web aims at using formal syntax with well-defined semantics for improving this process. Instead of text pages, it allows people to publish formal expressions according to some background theory (called ontology).
Working with the semantic web requires to import or transform semantic web expressions to use it in a new context. For instance, using information coming from a corporate source to integrate it in a portfolio management system. But there is no reason that this information is described in the same language with regard to the same ontology. It is thus necessary to transform the knowledge from one formalism to another (very often using language rewriting).
Obviously, this must be done in accordance with the semantics of the language. However, it is not easy to know if a particular transformation satisfies a particular property (e.g., preserving the models of a representation).
We would like to investigate the Proof-Carrying Code principle in the context of transformation engineering. This principle consists of attaching proofs of satisfied properties to transformations and checking these proofs before using the transformations. This is also useful to prove properties of transformations designed by composing other transformations.
The goal of this post-doctoral stay is to investigate further these principles and to design a framework (based on existing tools) in which "proof-carrying transformations" could be embedded within the semantic web infrastructure.
The successful candidate will have to investigate this framework, as well as to evaluate available tools and adapt them to our context. Possible tools include OMDoc for expressing proofs on the web, Elan rewriting system, Coq and Prosper proof environments.
Candidates must have a Ph.D. in Computer Science or related discipline, with research background in at least one of the following: logic, theorem proving, automated deduction, knowledge representation.
The position is located at INRIA Rhône-Alpes, Montbonnot (near Grenoble, France) a main computer science research lab, in a stimulating research environment. Research will be carried out in the Exmo team under the supervision of Jérôme Euzenat.
References:
INRIA Priority research themes:
Qualification: PhD or equivalent in computer science
Researched skills:
Hiring date: September 2005
Place of work: Montbonnot (38) very close to Grenoble
Duration: 12 months
Salary: 2150 EUR/month
Contact For further information, contact Jerome . Euzenat A inrialpes . fr.
Procedure: Visit INRIA's presentation (including FAQ and forms).