Technical Articles / Opinions / News / Projects

A Series on Strongly-Specified Functions in Coq

Using dependent types and the Prop sort, it becomes possible to specify functions whose arguments and results are constrained by properties. Using such a “strongly-specified” function requires to provide a proof that the supplied arguments satisfy the expected properties, and allows for soundly assuming the results are correct too. However, implementing dependently-typed functions can be challenging. In this series, we explore several approaches available to Coq developers.

Implementing Strongly-Specified Functions with the refine Tactic
Implementing Strongly-Specified Functions with the Program Framework