|
13406
|
1 |
@Article{Berger-JAR-2001,
|
|
|
2 |
author = {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger},
|
|
|
3 |
title = {The {Warshall} Algorithm and {Dickson's} Lemma: Two
|
|
|
4 |
Examples of Realistic Program Extraction},
|
|
|
5 |
journal = {Journal of Automated Reasoning},
|
|
|
6 |
publisher = {Kluwer Academic Publishers},
|
|
|
7 |
year = 2001,
|
|
|
8 |
volume = 26,
|
|
|
9 |
pages = {205--221}
|
|
|
10 |
}
|
|
|
11 |
|
|
|
12 |
@TechReport{Coquand93,
|
|
|
13 |
author = {Thierry Coquand and Daniel Fridlender},
|
|
|
14 |
title = {A proof of {Higman's} lemma by structural induction},
|
|
|
15 |
institution = {Chalmers University},
|
|
|
16 |
year = 1993,
|
|
|
17 |
month = {November}
|
|
|
18 |
}
|
|
17025
|
19 |
|
|
|
20 |
@InProceedings{Nogin-ENTCS-2000,
|
|
|
21 |
author = {Aleksey Nogin},
|
|
|
22 |
title = {Writing constructive proofs yielding efficient extracted programs},
|
|
|
23 |
booktitle = {Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics},
|
|
|
24 |
year = 2000,
|
|
|
25 |
editor = {Didier Galmiche},
|
|
|
26 |
volume = 37,
|
|
|
27 |
series = {Electronic Notes in Theoretical Computer Science},
|
|
|
28 |
publisher = {Elsevier Science Publishers}
|
|
|
29 |
}
|
|
25426
|
30 |
|
|
|
31 |
@Article{Wenzel-Wiedijk-JAR2002,
|
|
|
32 |
author = {Markus Wenzel and Freek Wiedijk},
|
|
|
33 |
title = {A comparison of the mathematical proof languages {M}izar and {I}sar},
|
|
|
34 |
journal = {Journal of Automated Reasoning},
|
|
|
35 |
year = 2002,
|
|
|
36 |
volume = 29,
|
|
|
37 |
number = {3-4},
|
|
|
38 |
pages = {389-411}
|
|
|
39 |
}
|