[Matryoshka-devel] TACAS 2017

Jasmin Blanchette jasmin.blanchette at gmail.com
Tue Dec 27 10:50:54 CET 2016

Dear all,

Haniel wrote:

> I am glad to inform you that our paper (with Pascal and Andrew)
> "Congruence Closure with Free Variables" has been accepted to TACAS
> 2017. A draft is already available on Matryoshka's web site; a version
> taking into account the reviewers' comments will be available
> mid-january.

This is great news! Congratulations! The TACAS paper is a theoretically and practically nice generalization of my favorite paper of 2014, by Andy, Cesare, and Leo (FMCAD 2014, "Finding conflicting instances of quantified formulas in SMT"). The results on Sledgehammer-generated problems are very impressive, both with CVC4 and with veriT.

We had another Matryoshka-related submission at an ETAPS conference, "A lambda-free higher-order recursive path order", with Daniel, Uwe, and me as authors. I'm glad to report that it has been accepted at FoSSaCS. The paper shows that it's possible to smoothly extend the recursive path order from first-order terms to lambda-free higher-order terms (also called applicative first-order terms). We also have a draft about a transfinite Knuth-Bendix order. All these results have been formalized in Isabelle.



More information about the matryoshka-devel mailing list