From Proposition to Program - Embedding the Refinement Calculus in Coq.

Wouter Swierstra, Joo Alpuim

Browse the full FLOPS paper archive.