[tschottdorf]

https://github.com/uwplse/verdi is a good example of this (it uses coq and extractions along with minimal glue).

[unboxed_type]

Have you tried it yourself or maybe you know someone who have? Honestly, I think that this development is highly impractical due to very high entrance ticket price for someone not belonging to UW PLSE group ;-)