@Article{Berger-JAR-2001,
author = {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger},
title = {The {Warshall} Algorithm and {Dickson's} Lemma: Two
Examples of Realistic Program Extraction},
journal = {Journal of Automated Reasoning},
publisher = {Kluwer Academic Publishers},
year = 2001,
volume = 26,
pages = {205--221}
}
@TechReport{Coquand93,
author = {Thierry Coquand and Daniel Fridlender},
title = {A proof of {Higman's} lemma by structural induction},
institution = {Chalmers University},
year = 1993,
month = {November}
}
@InProceedings{Nogin-ENTCS-2000,
author = {Aleksey Nogin},
title = {Writing constructive proofs yielding efficient extracted programs},
booktitle = {Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics},
year = 2000,
editor = {Didier Galmiche},
volume = 37,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers}
}
@Article{Wenzel-Wiedijk-JAR2002,
author = {Markus Wenzel and Freek Wiedijk},
title = {A comparison of the mathematical proof languages {M}izar and {I}sar},
journal = {Journal of Automated Reasoning},
year = 2002,
volume = 29,
number = {3-4},
pages = {389-411}
}