Engineer for providing interoperability among computational logic systems
| ||||
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. | ||||
| ||||
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 |