** Post-doc announcement (expanded version ) **
RAPIDO -- Reasoning And Programming with Infinite Data-Objects.
http://www.irif.fr/~saurin/RAPIDO
* postdoc positions in RAPIDO project:
We are opening one post-doc position, starting between october 2018 and
january 2019.
The post-doc will join the RAPIDO project, which is aimed at studying
logical methods and tools for enhancing reasoning and programming on
infinite data.
RAPIDO is an ANR-funded project involving researchers from three french
labs: IRIF (Paris), LIP (Lyon) and LSV (Cachan). It is coordinated by
Alexis Saurin (IRIF lab, saurin@irif.fr) and the post-doc position will
administratively be hosted by Paris Diderot University.
RAPIDO aims at gathering young researchers to investigate the
applicability of proof-theoretical methods to reason and program on
infinite data objects. The goal of the project is to develop logical
systems capturing infinite proofs (proof systems with least and greatest
fixed points as well as infinitary proof systems), to design and to study
programming languages for manipulating infinite data such as streams both
from a syntactical and semantical point of view. Moreover, the ambition of
the project is to apply the fundamental results obtained from the proof-
theoretical investigations (i) to the development of software tools
dedicated to the reasoning about programs computing on infinite data,
e.g. stream programs (more generally coinductive programs), and (ii) to
the study of properties of automata on infinite words and trees from a
proof-theoretical perspective with an eye towards model-checking problems.
* Topics and requirements for applicants
We are looking for young researchers who can contribute to the research
topics of RAPIDO. Candidates should hold a PhD in computer science or a
closely related field (or be close to complete their PhD) with skills in
formal methods and logic and a strong expertise in at least one of the
following topics:
*********
automata theory, coinduction, cyclic and infinitary
proofs, denotational semantics, functional programming,
games and game semantics, infinitary rewriting, lazy
evaluation, linear logic, MSO logic, proof assistants
proof theory, realizability, streams, temporal logics.
*********
We will be especially particularly interested in applications by
candidates who have an experience using the Coq proof assistant, even
though this shall by no mean refrain someone to apply!
* Inter-group project/collaborations
Since the project involves members of several french labs, it will
be particularly welcome is the post-doc can collaborate with
participants of at least two labs, thus fostering collaborations between
sites. The montly "CHOCOLA" meeting in ENS Lyon may be an occasion for
that, as well as extended visits to other sites).
* Application submission guidelines
Applications should be sent to Alexis Saurin before July 18th 2018
in an email entitled "RAPIDO postdoc application", providing:
- a detailed CV with a publication list,
- a research statement of at most two pages plus bibliography,
- and one or two recommendation letters.
Potential candidates are strongly encouraged to contact the project
coordinator (together with other project members) for informal
enquiries as soon as as the announcement is released, when *starting*
to prepare their application (such as starting dates, connections with
project sites, salary...).
More details on RAPIDO project, its members as well as the present
postdoc positions can be found at:
http://www.irif.fr/~saurin/RAPIDO
* Important dates:
Informal enquiries: as soon as possible
Application deadlines: july 18th 2018
Starting date: between october 2018 and january 2019.