Internships

Summer Internship 2014

Abstract Sledgehammer is a powerful interface from Isabelle to automated provers, to discharge subgoals that appear during the interactive proofs. It chooses facts related to this goal and asks some automatic provers to find a proof. The proof can be either reconstructed or just used to extract the relevant lemmas: in both cases the proof is not trusted. We extend the support by adding one first-order prover (Zipperposition), the reconstruction for two higher-order ATPs (Leo-II and Satallax) and an SMT solver veriT. The support of higher-order prover should especially improve Sledgehammer's performance for higher-order goals.

My report, bibtex and the presentation (both in English)

Summer Internship 2013

Abstract:We present a formalization proof of Uno and Yagiura's algorithm, using the theorem proving assistant Coq. This is a fundamental combinatorial algorithm which operates over permutation. Direct applications include computational biology (e.g. heuristics in estimating the genealogical distance between two species), text processing (e.g. generating the synchronous context-free grammar of two sequences with many-to-many alignment links ), the problem has been generalized to d permutations by Heber and Stoye, ... This text is part of an internship project which took place at LIP6, Université Pierre & Marie Curie, Paris, under the joint supervision of B.M. Bui-Xuan and F. Peschanski.

My report (in English) and the corresponding Beamer presentation (in French)