@article{Paulin_Mohring_1993,
    doi = {10.1016/s0747-7171(06)80007-6},
    url = {https://doi.org/10.1016%2Fs0747-7171%2806%2980007-6},
    year = {1993},
    month = {may},
    publisher = {Elsevier {BV}},
    volume = {15},
    number = {5-6},
    pages = {607--640},
    author = {Christine Paulin-Mohring and Benjamin Werner},
    title = {Synthesis of {ML} programs in the system Coq},
    journal = {Journal of Symbolic Computation}
}

@article{Paulin_Mohring_1993, doi = {10.1016/s0747-7171(06)80007-6}, url = {https://doi.org/10.1016%2Fs0747-7171%2806%2980007-6}, year = {1993}, month = {may}, publisher = {Elsevier {BV}}, volume = {15}, number = {5-6}, pages = {607--640}, author = {Christine Paulin-Mohring and Benjamin Werner}, title = {Synthesis of {ML} programs in the system Coq}, journal = {Journal of Symbolic Computation} }