Ingénieur de développement pour l'interopérabilité dans les systèmes logiques du calcul

Type de poste : Ingénieur

Lieu de travail : Paris-Saclay

Thème de recherche : Algorithmique, programmation, logiciels et architectures

Projet : PARSIFAL

A propos de l'INRIA et du poste

L’INRIA est un institut de recherche spécialisé dans les sciences et technologies de l'information et de la communication (STIC). 3600 personnes travaillent dans ses centres de recherche implantés dans sept régions. Le centre de recherche de Saclay compte environ 200 personnes, réparties dans une dizaine d’équipes de recherche et dans des services d'appui à la recherche.  L'équipe de recherche Parsifal travaille sur la logique de calcul et la structure des preuves formelles. Bien qu'une grande partie de l'équipe de recherche est théorique, membres de l'équipe ont participé à la construction d'un certain nombre de systèmes informatiques de ces dernières années pour mettre en œuvre une variété de sujets. S'agit notamment d'un langage de programmation logique (λProlog), un model checker (Bedwyr), et les assistant de preuve (Abella, Tac). Bien que tous ces systèmes sont mis en œuvre dans le langage de programmation (OCaml) même et tous les aspects d'application de la même logique, ils ne sont pas actuellement en mesure d'interopérer. Il ya, cependant, plusieurs applications dans lesquelles la coordination de ces outils est très utile.  Pour plus d'informations sur Parsifal et ces systèmes logiciels, visite http://www.lix.polytechnique.fr/parsifal/.

Mission

L'ingénieur participera à la conception et la mise en œuvre de diverses nouvelles langues formelles, qui peuvent être utilisés par ces systèmes d'interaction. Ces langages formels pourraient être basés sur une syntaxe logique existante ou XML. Le plan est de ne pas toucher les «logic engines» dans les systèmes existants et de développer des moyens pour eux de communiquer les uns avec les autres. L'ingénieur sera également responsable de la conception des «front-end» qui prennent diverses contributions d'un utilisateur d'envoyer et de récupérer des informations provenant de ces systèmes existants. De cette façon, les outils de raisonnement sur des langages de programmation peuvent être développés.

Descriptif du poste

The engineer will participate with other team members and their colleagues in developing means for these various systems to interoperate. In particular, the following specific tasks are envisioned:

● develop new grammars that the various systems can use

● implement the associated parsers, printers, and type checkers

● make modifications to the functionality of existing systems so that these new means of communicating are directly supported

● do the coding in OCaml and the associated suite of tools

● assist in the development and documentation of new examples and test cases

● make the software and examples available on the web

● help in moving the prototype systems to more mature status

Profil recherché

● Training in computer systems and knowledge of software development and related tools (version manager, compiling, documentation, testing, debugging, …

● Experience in using OCaml and associated utilities (for example, parser generators).

● English language skills, sufficient for daily working and writing in English (the team at LIX is international and our many close colleagues are from several countries)

● Version control systems (SVN) and documentation preparation (Latex, HTML)

● Familiarity with Linux and the basics of web pages development and publishing.

● Some familiarity with symbolic computing and, possibly, logic.

Avantages

Lieu de travail :

Laboratoire d'Informatique, LIX

École Polytechnique, Route de Saclay

91128 PALAISEAU Cedex FRANCE

Informations complémentaires

Contact Scientifique : Dale Miller, dale.miller@inria.fr , Team Leader, Parsifa

Contact administratif : Marie Domingues, marie.domingues@inria.fr