Post-doc position: Transformation proofs on the semantic web

Post-doctoral position
Transformation proofs on the semantic web
http://www.inrialpes.fr/exmo/training/PD-2004-TPSW.html

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.

It then becomes necessary to import or transform semantic web 
expressions to use it in a new context. For instance, using 
information comming from a corporate source to integrate it in a 
portfolio management system. For that purpose, one uses 
transformations 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 successful candidate will have to investigate this problematic, 
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 [1] under the supervision of Jérôme Euzenat.

References:
[1] http://www.inrialpes.fr/exmo
[2] http://www.semanticweb.org/SWWS/program/full/paper16.pdf

-- 
  Jérôme Euzenat                  __
                                  /      /\
  INRIA Rhône-Alpes,            _/  _   _   _ _    _
                               /_) | ` / ) | \ \  /_)
  655, avenue de l'Europe,    (___/___(_/_/  / /_(_________________
  Montbonnot St Martin,       /        http://www.inrialpes.fr/exmo
  38334 Saint-Ismier cedex,  /
  France____________________/   Jerome . Euzenat (à) inrialpes . fr

Received on Tuesday, 9 March 2004 04:56:05 UTC