Title
  Provably algorithmic schemes in functional programming:
  application to interactive computations


The thesis considers the development in OCaml of higher-order
functions that, thanks to functional programming, implement
algorithmic schemes with provable performances.  Performance
objectives vary depending on the scheme: eg work (number of operations
performed), or memory or parallel depth or number of cache misses or
reliability; generally a tradeoff between several criteria.
Functional programming provides both constructive and executable
semantics.  Furthermore the clear description of the computation
facilitates proofs of program correctness and yet authorizes
transformation schemes for performance tuning from cost models.
The primary objective is provide, thanks to Coq, proved
implementations of those schemes.

While classical schemes will be considered (memoization [1],
map-reduce [3], cache [4], work-stealing, anytime), the thesis will
mainly focus on provable randomization schemes [2], especially
homomorphic hashing (eg polynomial evaluation from Schwartz-Zippel
lemma).  For such computations, the probability may be tuned based on
several independent executions, a particular case of Map-Reduce.

Yet considering composition of several randomized algorithms,
efficient functional evaluation techniques to reach an arbitrary error
probability will be formalized and developed.  A possible target
application of those randomized schemes is to improve the work on
polynomial inequalities [5].

Finally, the thesis will investigate interactive proofs that are based
on the interaction of a proved randomized verifier and an outsourced
untrusted prover; here a possible target may be efficient (polynomial)
probabilistic proofs of tautologies (non-SAT).


Candidate's skills: algorithms and programming; functionnal
programming, Ocaml; formal proof, Coq; background in mathematics
(probabilities, arithmetics and algebra). A strong motivation for the
development of proved software is expected.  Typical profiles:
- very good capabilities in maths
  + strong motivation on formal proofs and Coq
- excellent results in relevant aspects of computer science
  + strong motivation on relevant maths

  
Candidates are invited to send their application via email to
- Jean-François Monin <jean-francois.monin@imag.fr>
- Jean-Louis Roch <jean-louis.roch@imag.fr>
- Pierre Corbineau <pierre.corbineau@imag.fr>
Please include a CV, a motivation letter and contact information
for 1 or 2 referees.


Bibliography
[1] Implementing and reasoning about hash-consed data structures in Coq.
    Thomas Braibant, Jacques-Henri Jourdan, David Monniaux.
[2] Proofs of randomized algorithms in Coq.
    Philippe Audebaud, Christine Paulin-Mohring
[3] Modeling and optimizing MapReduce programs.
    Jens Dörre, Sven Apel, Christian Lengauer.
    Concurrency and Computation:Practice and Experience, 27(7), May 2015
[4] Cache and I/O efficent functional algorithms.
    Guy E. Blelloch and Robert Harper. POPL 2013
[5] On the Generation of Positivstellensatz Witnesses in Degenerate Cases.
    David Monniaux, Pierre Corbineau. ITP 2011.