Engineer for providing interoperability among computational logic systems

Job Type: Engineering

Location: Paris-Saclay

Research topic: Algorithms, programming, software and architecture

Project: PARSIFAL

About INRIA and the position

INRIA is a research institute specializing in the science of information technology and communications.  3600 people work in research centers located in seven regions. The research center of Saclay has about 200 people spread over dozens of research teams and support services.. The Parsifal research team is working on computational logic and the structure of formal proofs.  Although much of their research work is theoretical, team members have participated in the construction of a number of computer systems in recent years to implement a variety of topics. These include a logic programming language (λProlog), a model checker (Bedwyr), and two proof assistants (Abella, Tac). Although all these systems are implemented in the programming language (OCaml) and they all deal with the same logic, they are not currently able to interoperate. There are, however, several applications in which the coordination of these tools is necessary.  For more information about Parsifal and these systems software, visit http://www.lix.polytechnique.fr/parsifal/.

Mission

The engineer will participate in the design and implementation of various new file formats to get these systems to interact. These file format   may be based on existing logical syntax or XML. The plan is to not touch the "logic engines" in existing systems but to develop ways for them to communicate with each other. The engineer will also be responsible for the design of “front-ends” that take various inputs from a user and then to send and retrieve information from these computational systems.  One such too we envision will be used to reason about the operational and static properties of programming languages.

Description of post

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

Desired Profile

● Training in computer systems and knowledge of software development and related tools (version control, 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.

Location

Workplace: Laboratoire d'Informatique, LIX

Ecole Polytechnique, Route de Saclay

91128 Palaiseau Cedex FRANCE

Additional information

Scientific contact: Dale Miller, dale.miller @ inria.fr, Team Leader, Parsifal

Administrative Contact: Marie Domingues marie.domingues @ inria.fr