Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq.

Dominique Larchey-Wendling, Jean-Franois Monin

Browse the full ITP paper archive.