Pierre-Évariste Dagand

Partial type equivalences for verified dependent interoperability

2016 · ACM SIGPLAN Notices

Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading …