[Matryoshka-devel] Draft & preprint

Blanchette, J.C. j.c.blanchette at vu.nl
Tue Mar 28 12:22:01 CEST 2017

Dear colleagues,

Two news items:

1. We will submit an extended version of our IJCAR 2016 paper about a verified SAT solver to the special issue of JAR on milestones of formalization. The current draft is available here:


The article includes a refinement to imperative ML code, using Imperative HOL and the Refinement Framework, and uses the two-watched-literal data structure. We will submit the paper on Friday afternoon but will also accept feedback afterwards.

2. Our LICS 2017 submission on foundational nonuniform (co)datatypes has been accepted! The current version is available at


The camera-ready version is due in a few weeks from now.



More information about the matryoshka-devel mailing list