19 Sep 2023

Job Information

Organisation/Company

TSP - Telecom SudParis

Department

Electronics and Physics dept. (EPh)

Research Field

Physics

Researcher Profile

First Stage Researcher (R1)

Country

France

Application Deadline

18 Oct 2023 - 00:00 (Europe/Paris)

Type of Contract

Temporary

Job Status

Full-time

Hours Per Week

39

Offer Starting Date

19 Oct 2023

Is the job funded through the EU Research Framework Programme?

Not funded by an EU programme

Reference Number

Post-doc EPH

Is the Job related to staff position within a Research Infrastructure?

No

Offer Description

MISSIONS

This position takes place within the ANR project ICSPA (https:// icspa.inria.fr/), which seeks to improve trust in proof assistants based on set theory (B method, TLA+). To do this, the idea is to export proofs found by such tools into the Dedukti logical framework, and also to import proofs from Dedukti into these assistants. By having the proof verified in Dedukti, we increase confidence in what the assistant claims. In the other direction, this enables the proofs to be certified for industrial use. Finally, by moving down from one assistant to Dedukti and then up again to another, this enables interoperability between them.

This position focuses on the Atelier B tool developed by Clearsy (a member of the ANR project consortium).

Members of the ICSPA project have developed an encoding of Theory B in Dedukti. In this encoding, it is possible to translate the proof obligations of Atelier B, as well as to search for proofs of these obligations. However, the best solution would be to be able to translate the proofs found by Atelier B directly into Dedukti. To do this, it is proposed that Atelier B should first be instrumented to write a trace containing sufficient information to be able, in a second phase, to reconstruct a complete proof in Dedukti. For this reconstruction, if possible, automated theorem provers able to generate Dedukti proofs will be used.

Furthermore, if there is a Dedukti proof of an encoding of a theory B formula, regardless of how it was obtained, we would like to be able to import it into Atelier B. To do this, we will need to use the mechanisms of Aterlier B to simulate the typing verification performed by Dedukti.

ACTIVITIES

The candidate will be required to carry out the following tasks:

working with Clearsy to instrument the Atelier B tool in order to recover a proof trace ;

reconstruction of the proof trace in Dedukti ;

import of Dedukti proofs, using the encoding of B in Dedukti, into Atelier B.

The candidate will collaborate with all people involved in the ICSPA project.

Requirements

Research Field

Physics

Education Level

PhD or equivalent

Skills/Qualifications

Level of training and / or experience required

PhD or Doctorat for less than 3 years

Essential skills, knowledge and experience

Knowledge in logics for computer science

Experience in mechanized theorem proving

Good level in programming (if possible, using OCaml)

Advantageous skills, knowledge and experience

Knowledge of a proof assistants

Knowledge of the B method

Knowledge in automated theorem proving

Abilities and skills

Strong motivation for research

Ability to work in a team

Spirit of initiative and creativity, autonomy

Languages

ENGLISH

Level

Excellent

Research Field

Physics

Additional Information

Benefits

Application deadline: October 18th, 2023

Nature of the contract: 12-months

To apply, please send us a CV, a cover letter and a summary of your doctoral thesis

Location of the position : Evry -Courcouronnes and Palaiseau (France)

The positions offered for recruitment are open to all with, on request, accommodations for candidates with disabilities

Working conditions: Teleworking possible, restaurant and cafeteria on site, accessibility by public transport (with employer's participation) or close to main roads, staff association and sports association on campus

Website for additional job details

https: // institutminestelecom.recruitee.com/l/en/o/offre-type-telecom- sudparis-t…

Work Location(s)

Number of offers available

1

Company/Institute

Télécom SudParis

Country

France

State/Province

Ile-de-France

City

Evry-Courcouronnes

Postal Code

91000

Street

9 rue Charles FOURIER

Geofield

Where to apply

Website

https: // institutminestelecom.recruitee.com/l/en/o/offre-type-telecom- sudparis-t…

Contact

State/Province

Ile-de-France

City

Evry-Courcouronnes

Website

https: // www. telecom-sudparis.eu/

Street

9 rue Charles FOURIER

Postal Code

91000

E-Mail

[email protected]

STATUS: EXPIRED