[Matryoshka-devel] Ehoh

Petar Vukmirovic petar.vukmirovic2 at gmail.com
Thu Sep 27 18:39:16 CEST 2018


Dear colleagues,

I would like to share with you the draft of the paper we plan to submit to
TACAS 2019:

Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan
Schulz.

Shorter, conference version of the draft is available at:
http://matryoshka.gforge.inria.fr/pubs/ehoh_paper.pdf, whereas report
version
is available at http://matryoshka.gforge.inria.fr/pubs/ehoh_report.pdf.

The paper explains how a state of the art prover can be extended to a
higher-order logic.
We managed to do so while having near-to-0 overhead and beating encoding
based approaches.

If you're interested in the paper, we would be super thankful if you could
give us some
comments :) Links given above will be periodically refreshed with updated
versions
of the paper.

Cheers,
Petar.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20180927/de6a6841/attachment.html>


More information about the matryoshka-devel mailing list