PhD Position, fully funded - The Matryoshka Project

[Cláudia Nalon]

----

Matryoshka is an ambitious research project that aims at developing
efficient deduction techniques and integrating them in proof assistants.
The project is funded by a European Research Council Starting Grant from
March 2017 to February 2022. It is co-located between Vrije Universiteit
Amsterdam (Jasmin Blanchette) in the Netherlands and Loria, Inria Nancy
- Grand Est (Stephan Merz, Pascal Fontaine) in France.

Proof assistants are increasingly used to verify hardware and software
and to formalize mathematics. However, despite the success stories, they
remain very laborious to use. To make interactive verification more
cost-effective, we propose to deliver powerful automation to users of
proof assistants by fusing and extending two lines of research:
automatic and interactive theorem proving. To reach end users, these new
provers will be integrated in proof assistants, including Coq,
Isabelle/HOL, and the TLA+ Proof System. The subject of the position
advertised here is this last aspect, i.e. integrating automatic
deduction techniques in the TLA+ Proof System, the proof assistant for
Lamport's Temporal Logic of Actions. To provide more automation for the
non-temporal aspects of TLA+, which make up perhaps 90% or more of
typical proofs, the PhD student will design efficient translations of
set theory to higher-order logic. In order to filter the few useful
lemmas out of the large TLA+ context, we suggest the design and use of a
system of soft types.

We are looking for one outstanding candidate for a Ph.D. due to start
before the end of 2018. Candidates should ideally have some experience
with automatic or interactive theorem proving and be at ease with both
theory and engineering. The student will work in a motivating
environment in close collaboration with the Matryoshka and TLA teams.
Please contact as soon as possible Jasmin Blanchette
(Jasmin.B...@inria.fr),
Pascal Fontaine (Pascal....@loria.fr) and Stephan Merz
(Stepha...@loria.fr)
for more information.

To know more:

* the Matryoshka project [1]
* the VeriDis team [2]
* TLA [3]
* TLAPS [4]
* the Inria-Microsoft project, Tools for Proofs [5]



Links:
------
[1] http://matryoshka.gforge.inria.fr/
[2] http://veridis.loria.fr/
[3] http://lamport.azurewebsites.net/tla/tla.html
[4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html
[5] https://www.msr-inria.fr/projects/tools-for-proofs/

--
Cláudia Nalon
------------------------------------
Departmento de Ciência da Computação
Instituto de Ciências Exatas
Universidade de Brasília
http://www.cic.unb.br/~nalon