[Matryoshka-devel] Some Matryoshka news

Jasmin Blanchette jasmin.blanchette at inria.fr
Fri Nov 11 00:35:15 CET 2016


Dear colleagues,

First, I'm going to refer to everybody on this list (or in CC:) by first name. It may be helpful to take a peek at

	http://matryoshka.gforge.inria.fr

to see who's who.

Now, some news.

1. As you might have discovered from glancing at the Matryoshka web page, Matryoshka has made its first hire: Alexander Bentkamp. He will start his Ph.D. on 1 March 2017 at VU Amsterdam, on a four-year contract. In the Isabelle community, he is known for his impressive contributions to the Archive of Formal Proofs:

	https://www.isa-afp.org/entries/Deep_Learning.shtml
	https://www.isa-afp.org/entries/Latin_Square.shtml

The Deep Learning formalization is the basis of his M.Sc. thesis and will form the basis of a submission next year. At over 200 pages in PDF format, it is very substantial. And SMT solvers in particular were very helpful to develop the proof.

Alex will work on general techniques for higher-order reasoning and probably also contribute to the higher-order superposition calculus and/or prover. I am confident that this crucial part of the project will be in very capable hands.

2. Haniel, Pascal, and Andy (= Andrew) have submitted a nice paper about quantifier instantiation in SMT solvers, with implementations in the solvers CVC4 and veriT. This will have a nice impact on proof obligations arising in interactive verification. See

	https://members.loria.fr/HBarbosa/papers/barbosa2016-extended.pdf

3. Since April, a loose federation of superposition guys and formalizers have been working on lambda-free higher-order RPO and transfinite KBO (TKBO) with subterm coefficients. I finished the RPO proof, in Isabelle, a few months ago and two days ago, I finished the TKBO proof as well. The former is already in the Archive of Formal Proofs

	https://devel.isa-afp.org/entries/Lambda_Free_RPOs.shtml

and is the basis of a conference submission with Daniel and Uwe:

	http://people.mpi-inf.mpg.de/~jblanche/lambda_free_rpo_conf.pdf
	http://people.mpi-inf.mpg.de/~jblanche/lambda_free_rpo_rep.pdf

TKBO remains to be written. The syntactic ordinal library that emerged for TKBO will be the object of a third conference submission (!), with Mathias and Dmitriy.

Don't hesitate to post to the list whenever there are exciting developments you want to share or if you want to react. This applies to all of you, irrespective of which bucket your name ended up in on the Matryoshka web page. In particular, it would be nice if we could all get into the habit of telling the world about our submissions and/or accepted papers, if they are vaguely connected to Matryoshka.

Cheers,

Jasmin



More information about the matryoshka-devel mailing list