@inproceedings{LM3,
title = { {Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq} },
author = {Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
year = {2023},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
address = {Dagstuhl, Germany},
annote = {Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml},
pages = {21:1--21:17},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {268},
team = {PACSS},
urn = {urn:nbn:de:0030-drops-183963},
}
