[TYPES/announce] Post Doc available, University of Bologna

[Dale Miller]

Research grant at the Department of Computer Science and Enginnering of
University of Bologna

Dear All,

The Department of Computer Science and Enginnering of the University of
Bologna is about to open a post-doctoral position on:

  Design and Implementation of a Constraint Logic Programming Language
  based on Lambda-Prolog

- Contact for inquiries or application: Prof. Claudio Sacerdoti Coen
  <claudio.sacerdoticoen at unibo.it>
- Duration: 1 year
- Starting date: the starting date is flexible
- Keywords: constrained logic programming, binders, higher-order programming,
  interactive theorem proving
- Location: Department of Computer Science and Engineering
  http://www.cse.unibo.it/en
  University of Bologna http://www.unibo.it/en/homepage
- Collaborations: the research activity is part of a larger project with
  Prof. Dale Miller, INRIA Saclay - Île-de-France
  Dr. Enrico Tassi, INRIA Sophia-Antipolis
  It will be possible to temporarily visit the two sites for short periods.

The gross salary of the research fellowship contract is EURO 26.174,00 per annum.
The salary is exempt of withholding tax and includes all statutory social
security charges the Research Fellow is subject to (the research fellow has to
pay ~10% of taxes only).

The starting date is flexible. The contract is renewable for one year.

The applicant must have a PhD in computer science with a strong background on
the implementation of (logic) programming languages. Further knowledge on
constraint programming, static interpretation of programs and interactive
theorem proving is a plus.

Description of the research activity:
  The middle term goal is the certified implementation of an interactive
  theorem prover like Coq (http://coq.inria.fr) or Matita
  (http://matita.cs.unibo.it) using a constraint logic programming language.
  The logic part of the language needs to deal with higher order abstract
  syntax and binders to raise the level of abstraction of the implementation.
  The constraint handling part will deal with the proof obligations that are
  opened during an interactive proof. The flavour of constraint programming
  will be novel: the constraints are not pre-determined by the language, but
  are dynamically described by the user in the program itself. The constraint
  propagation rules are also described by the user as theorems, to be stated
  and proved in an extension of the theorem prover Abella
  http://abella-prover.org.

  We currently have a prototype based on an extension of the Lambda-Prolog
  language (http://www.lix.polytechnique.fr/~dale/lProlog/) to deal with
  that kind of constraints. The job of the applicant consists in re-designing
  the language extension and in reimplementing the prototype from scratch to
  maximize the performance and to integrate the constraint propagation rules
  in the most elegant way.

Please forward this email to possible applicants.

Best regards,
Claudio Sacerdoti Coen