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