@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}
}
