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).

근무 예정지

대표Grenoble INP(해외) : 46 Av. Félix Viallet, 38031 Grenoble

해외(프랑스) : France, Grenoble INP UGA

관련 키워드

Engineering

기관 정보

Grenoble INP

  • 기관유형

    대학교(해외)

  • 대표전화

    +33 4 76 57 45 00

  • 대표주소

    46 Av. Félix Viallet, 38031 Grenoble

  • 홈페이지

    바로가기

이런 공고는 어떠세요?

마감