lthms' avatar, a hand drawing looking person, wearing a headset, close to a window on a raining night
Thomas Letan
lthms · he/him

Did you come across something which caught your attention? Don’t hesitate to shoot me an email in my public inbox.

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 such functions can be challenging. In this series, we explore several approaches available to Coq developers.

Implementing Strongly-Specified Functions with the refine Tactic

We see how to implement strongly-specified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions' arguments and return value. It makes Coq type system very expressive.

Implementing Strongly-Specified Functions with the Program Framework

Program is the heir of the refine tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.