1 \begin{thebibliography}{10} |
|
2 |
|
3 \bibitem{coen92} |
|
4 Martin~D. Coen. |
|
5 \newblock {\em Interactive Program Derivation}. |
|
6 \newblock PhD thesis, University of Cambridge, November 1992. |
|
7 \newblock Computer Laboratory Technical Report 272. |
|
8 |
|
9 \bibitem{constable86} |
|
10 R.~L. Constable et~al. |
|
11 \newblock {\em Implementing Mathematics with the Nuprl Proof Development |
|
12 System}. |
|
13 \newblock Prentice-Hall, 1986. |
|
14 |
|
15 \bibitem{felty91a} |
|
16 Amy Felty. |
|
17 \newblock A logic program for transforming sequent proofs to natural deduction |
|
18 proofs. |
|
19 \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic |
|
20 Programming}, LNAI 475, pages 157--178. Springer, 1991. |
|
21 |
|
22 \bibitem{gallier86} |
|
23 J.~H. Gallier. |
|
24 \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem |
|
25 Proving}. |
|
26 \newblock Harper \& Row, 1986. |
|
27 |
|
28 \bibitem{huet78} |
|
29 G.~P. Huet and B.~Lang. |
|
30 \newblock Proving and applying program transformations expressed with |
|
31 second-order patterns. |
|
32 \newblock {\em Acta Informatica}, 11:31--55, 1978. |
|
33 |
|
34 \bibitem{alf} |
|
35 Lena Magnusson and Bengt {Nordstr\"{o}m}. |
|
36 \newblock The {ALF} proof editor and its proof engine. |
|
37 \newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs |
|
38 and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237. |
|
39 Springer, published 1994. |
|
40 |
|
41 \bibitem{martinlof84} |
|
42 Per Martin-L\"of. |
|
43 \newblock {\em Intuitionistic type theory}. |
|
44 \newblock Bibliopolis, 1984. |
|
45 |
|
46 \bibitem{nordstrom90} |
|
47 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. |
|
48 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. |
|
49 \newblock Oxford University Press, 1990. |
|
50 |
|
51 \bibitem{paulson87} |
|
52 Lawrence~C. Paulson. |
|
53 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
|
54 \newblock Cambridge University Press, 1987. |
|
55 |
|
56 \bibitem{isabelle-ZF} |
|
57 Lawrence~C. Paulson. |
|
58 \newblock {Isabelle}'s logics: {FOL} and {ZF}. |
|
59 \newblock Technical report, Computer Laboratory, University of Cambridge, 1999. |
|
60 |
|
61 \bibitem{pelletier86} |
|
62 F.~J. Pelletier. |
|
63 \newblock Seventy-five problems for testing automatic theorem provers. |
|
64 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. |
|
65 \newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135. |
|
66 |
|
67 \bibitem{takeuti87} |
|
68 G.~Takeuti. |
|
69 \newblock {\em Proof Theory}. |
|
70 \newblock North-Holland, 2nd edition, 1987. |
|
71 |
|
72 \bibitem{thompson91} |
|
73 Simon Thompson. |
|
74 \newblock {\em Type Theory and Functional Programming}. |
|
75 \newblock Addison-Wesley, 1991. |
|
76 |
|
77 \end{thebibliography} |
|