Grenoble INP

Post-doc

Researcher (W/M) in sofware engineering - VERIMAG

마감2025.03.21~2025.03.28 공유하기

채용 정보

접수 기간
2025.03.21 00:00~2025.03.28 20:00
접수 방법
이메일지원더보기
채용 구분
경력
고용 형태
계약직
지원 자격
박사
모집 전공
공학계열더보기
기관 유형
대학교
근무 지역
해외(프랑스)더보기

Skills/Qualifications

Core competencies:

Rust, formal semantics of programming languages (especially operational semantics), formal proofs in Coq, programming in OCaml.

The project will require relative autonomy, but also the ability to collaborate with a doctoral student who is formalizing the borrow-checker on the LLBC representation. It also require interaction with experts on the subject (such as Son Ho and Aymeric Fromherz)

Specific Requirements

Mainly on-site-work at the VERIMAG laboratory.

Subject: Formally verified compilation of a Rust subset Extend the formally verified compiler CompCert with a Rust front-end. This prototype compiler will take as input the LLBC representation generated by the Charon tool (from the official Rust compiler), itself developed by Son Ho during
his Phd at INRIA.

This will require to formalize in the Coq/Rocq proof assistant the different semantics proposed for LLBC in Son Ho's manuscript. And ultimately, translate this representation into Csharpminor representation of CompCert (introducing several passes if necessary).