Pascal.Fontaine at loria.fr
Wed Jul 12 11:01:14 CEST 2017
Dear Matryoshka Friends,
I have a few good news to share from Nancy.
First, we are very happy to announce that Daniel El Ouraoui, a master
student from MPRI (Master Parisien de Recherche en Informatique, the
main research CS master in Paris) and currently doing an internship with
Matryoshka on higher-order SMT, is joining Matryoshka as a PhD student,
starting October 2017! Jasmin and myself will be co-advisors.
Second, a few Matryoshka-related works have been accepted and will be
presented during this summer (they are available in some form on the
Matryoshka web site):
Scalable fine-grained proofs for formula processing
Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine.
Accepted at CADE 2017 (Gothenburg), and also as presentation only at
PxTP 2017 (Brasilia). This will be presented by Haniel.
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, and Xuan Tung Vu
Accepted at FroCoS 2017 (Brasilia), and also as presentation only at SC²
2017 (Kaiserslautern) and SMT 2017 (Heidelberg). I will present this.
Congruence closure with free variables
Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds.
We already announced the presentation of this at TACAS 2017. It is also
accepted as presentation only at SMT 2017 (Heidelberg) and as a poster
at FroCoS 2017 (Brasilia). This will be presented by Haniel.
There will be two Matryoshka-related talks at the ARCADE workshop 2017
Towards Strong Higher-Order Automation for Fast Interactive Verification
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz and Uwe
Making Automatic Theorem Provers more Versatile
And we are already making some progress on higher-order SMT!
Language and proofs for Higher-order SMT (work in progress)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El
Ouraoui and Pascal Fontaine
is accepted at PxTP 2017 (Brasilia). It is not decided yet who will
present but four authors will be in Brasilia.
As you can infer from above, many people from Nancy will travel the next
SMT workshop: Haniel, Thomas, Pascal
SC² workshop: Haniel, Thomas, Pascal
VTSA+SC² summer schools: Haniel, Hans-Jörg, Daniel, Thomas, Pascal
ARCADE+CADE: Haniel, Simon, Pascal
FroCoS: Haniel, Simon, Pascal
We hope to meet you at one of these events soon!
More information about the matryoshka-devel