Embedded second-order cone programming with radar applications. - Paul Mountcastle; Thomas Henretty; Aale Naqvi; Richard Lethin (HPEC, 2015)

A unified Coq framework for verifying C programs with floating-point computations. - Tahina Ramananandro; Paul Mountcastle; Benoît Meister; Richard Lethin (CPP, 2016)