Home Publications Talks Past Projects Teaching Hobbies

Dana N. Xu

Research Scientist (Chargé de Recherche, junior) of Gallium Team at INRIA Paris - Rocquencourt, a French National Research Institute.
To:

News

• Our group recruits postdocs in Feb each year. You are welcome to join me in fighting against program errors!
• Dana's Blog

Postdoc Projects Available

At Gallium, we conduct research on the design, formalization, and implementation of programming languages and systems. The Caml language embodies many of our research results. Our objective is to improve the reliability of software systems through:

• higher-level, safer, more expressive programming languages based on the functional programming paradigm;
• automatic error detection via type systems, contracts, logical assertions;
• better linguistic support for formal methods, especially machine-checked proofs of programs.

The candidate will conduct research in an ongoing project related to hybrid (i.e. both static and dynamic) contract checking for a pure functional language (based on System F). We would like to apply the idea to both a strict language (ML) and a lazy language (Haskell). Related materials include:

• Dynamic Contract Checking for OCaml (a tutorial)
• Static Contract Checking (should work for both strict and lazy languaage.)

Contracts give a way to blame precisely the function at fault, even in the presence of higher-order functions. Such information makes debugging easier. Basically, we would like to enhance a compiler such that it takes Contracts, Program, possibly also Lemmas as inputs and checks modularly whether each function in a program satisfies its contract. If so, the code generated by the compiler should never yield a run-time error; if not, meaningful error messages should be generated, (preferably) at compile-time or at run-time, to assist in debugging. We welcome applications from candidates who would like to explore various aspects of this field with us. Topics of interest (which are independent of each other) include:

1. Contract-directed test case generation (a sibling to QuickCheck for Haskell).
2. Contract-directed optimization (e.g. dead/redundant code elimination)
3. Extending the expressiveness of the existing contracts framework in several ways (recursive contracts, polymorphic contracts, contracts for data constructors, etc. come to mind).
4. Machine-checking the correctness of the existing contract semantics using Coq (or Isabelle/HOL, etc.). We have only a manual proof at the moment.

This list is not exhaustive: potential candidates are welcome to discuss related work topics with us. If you are interested, please contact François Pottier and me.

Last modified: 2010-01-15        Page designed by via OSWD, modified by Dana N. Xu.