[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
This is an announcement for a postdoctoral position in the CAVOC project
(Compositional Automated Verification for OCaml). The post-doc will take place
in Nantes, France. It will be co-supervised by Guilhem Jaber (Nantes Université
and Inria Gallinette team) and Gabriel Radanne (Inria CASH team, Lyon).
It aims to bring together approaches from abstract interpretation, model
checking, and game semantics to statically analyze OCaml code.
The successful candidate will be employed by Inria and work in the Gallinette
team
(https://urldefense.com/v3/__https://gallinette.inria.fr__;!!IBzWLUs!Xt6ct7q7jYcqvdJxa0TIzp7pOHKZgO040ZKWGrk-iGfcNN6a0xcWrWRAqkTv3cnrsOZSaqd_XzyAdtg1J7IEQ7jMu7Edkq8LAr40eTo$
<https://urldefense.com/v3/__https://gallinette.inria.fr/__;!!IBzWLUs!Xt6ct7q7jYcqvdJxa0TIzp7pOHKZgO040ZKWGrk-iGfcNN6a0xcWrWRAqkTv3cnrsOZSaqd_XzyAdtg1J7IEQ7jMu7Edkq8LrMo-wts$
>), at Nantes University. The position is for one year, and should start in
the first semester of 2024 (to be negociated). The salary will depend on the
candidate's prior research experience with a guaranteed minimum of ~2200€/month
after taxes. The working language can either be English or French.
We seek candidates holding a PhD in Computer Science or Mathematics, and with
expertise in programming language semantics, λ-calculi, type theory, functional
programming, abstract interpretation, compilation, model checking, or program
logic.
## Profile
The candidate should be familiar with formal approaches in programming language
design, notably type systems, semantics, and logic. More concretely, knowledge
of the OCaml programming language is expected, and a knowledge of abstract
interpretation or model checking would be highly appreciated.
This postdoc strongly relies on the fact that practical implementation should
have strong theoretical foundations and that further refinements of the theory
should get inspiration from the practical side.
## Application process
- Applications will be processed starting the 18th of December. Late
applications will be considered until the position is filled.
- You do not need to have defended your PhD thesis to apply, but you will need
to have obtained your PhD to start the contract.
- Candidates can send their application to Guilhem Jaber (guilhem dot jaber at
inria dot fr) and Gabriel Radanne (gabriel dot radanne at inria do fr) with a
subject containing “[CAVOC post-doc application]“.
- The application should contain a CV, two selected publications and two
contacts of reference persons (or reference letters if available).
## Context
The CAVOC project aims to develop a sound and precise static analyzer for
OCaml, that can catch large classes of bugs represented by uncaught exceptions.
The analyzer reasons compositionally on programs, in order to analyze them at
the granularity of a function or of a module. It takes into account the
abstraction properties provided by the type system and the module system of the
language: local values, abstracted definitions of types, parametric
polymorphism.
The main goal is to be sound in a strong way: if an OCaml module is considered
to be correct by the analyzer, then one will have the guarantee that no OCaml
code interacting with this module can trigger uncaught exceptions coming from
the code of this module.
To model the behaviour of a module, we rely on game semantics, where programs
formed by a module and a client of the module are modelled as
calls-and-returns interactions. A module is then represented as a transition
system that generates traces representing the interaction with any possible
client. This transition system is directly generated from the module's code
(implementation and signature), using an operational semantics. We have
implemented such an interactive semantics for a large fragment of OCaml, which
we are using to develop our prototype analyzer.
