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