Matryoshka 2018

First European Workshop on
Higher-Order Automated Reasoning

25–27 June 2018, Amsterdam, The Netherlands
Co-located with WAIT 2018

This workshop brings together researchers working on automated deductive techniques for higher-order logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higher-order automatic theorem provers Leo-III and Satallax, the Lean proof assistant, and metaprovers such as HOLyHammer and Sledgehammer.

With the Matryoshka project, we aim at designing a new generation of higher-order automatic theorem provers based on state-of-the-art first-order provers, including E, veriT, and CVC4, and to integrate them in popular proof assistants. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. We encourage researchers motivated by the same goals to get in touch with us, subscribe to the matryoshka-devel mailing list, and join forces.

The workshop succedes to the LPAR-05 workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), held in Montego Bay, Jamaica. The Matryoshka workshop series is conceived to be a meeting point for the Matryoshka team and colleagues working on the same challenge. It is an informal event. We expect to hold it at least once a year until the project's completion in 2023.

Please send an email to the organizers if you would like to give a talk, demonstrate a tool, or otherwise participate.

The workshop will take place on 25, 26, and/or 27 June 2018 in the W&N building of the Vrije Universiteit Amsterdam. The VU is easily accessible on foot from the Amsterdam Zuid station, a short train ride away from Amsterdam Airport Schiphol.

Matryoshka 2018 will take place the same week as the Fourth Workshop on Automated Inductive Theorem Proving (WAIT 2018).

Hotels in Amsterdam can be very expensive. Even the cheapest options often cost over 100 euros per night. The neighboring city of Amstelveen has more reasonably priced options (e.g., Ibis) and is located close to the VU campus, a few stops away by public transportation (tram line 5 or metro line 51).

To be determined.
Alexander Bentkamp (VU Amsterdam)
Jasmin Christian Blanchette (VU Amsterdam)
Alexander Bentkamp (VU Amsterdam)
Jasmin Christian Blanchette (VU Amsterdam)
Sander Dahmen (VU Amsterdam)
Pascal Fontaine (U. Lorraine)
Johannes Hölzl (VU Amsterdam)
This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No. 713999). We also want to thank Mojca Lovrencak for helping with the local organization.


      This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.