8 |
8 |
9 \bibitem{basin91} |
9 \bibitem{basin91} |
10 David Basin and Matt Kaufmann. |
10 David Basin and Matt Kaufmann. |
11 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison. |
11 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison. |
12 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical |
12 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical |
13 Frameworks}, pages 89--119. Cambridge University Press, 1991. |
13 Frameworks}, pages 89--119. 1991. |
14 |
14 |
15 \bibitem{boyer86} |
15 \bibitem{boyer86} |
16 Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and |
16 Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and |
17 Lawrence Wos. |
17 Lawrence Wos. |
18 \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms. |
18 \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms. |
19 \newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986. |
19 \newblock 2(3):287--327, 1986. |
20 |
20 |
21 \bibitem{camilleri92} |
21 \bibitem{camilleri92} |
22 J.~Camilleri and T.~F. Melham. |
22 J.~Camilleri and T.~F. Melham. |
23 \newblock Reasoning with inductively defined relations in the {HOL} theorem |
23 \newblock Reasoning with inductively defined relations in the {HOL} theorem |
24 prover. |
24 prover. |
25 \newblock Technical Report 265, University of Cambridge Computer Laboratory, |
25 \newblock Technical Report 265, August 1992. |
26 August 1992. |
|
27 |
26 |
28 \bibitem{church40} |
27 \bibitem{church40} |
29 Alonzo Church. |
28 Alonzo Church. |
30 \newblock A formulation of the simple theory of types. |
29 \newblock A formulation of the simple theory of types. |
31 \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. |
30 \newblock 5:56--68, 1940. |
|
31 |
|
32 \bibitem{coen92} |
|
33 Martin~D. Coen. |
|
34 \newblock {\em Interactive Program Derivation}. |
|
35 \newblock PhD thesis, University of Cambridge, 1992. |
|
36 \newblock Computer Laboratory Technical Report 272. |
|
37 |
|
38 \bibitem{constable86} |
|
39 R.~L. {Constable et al.} |
|
40 \newblock {\em Implementing Mathematics with the Nuprl Proof Development |
|
41 System}. |
|
42 \newblock 1986. |
|
43 |
|
44 \bibitem{davey&priestley} |
|
45 B.~A. Davey and H.~A. Priestley. |
|
46 \newblock {\em Introduction to Lattices and Order}. |
|
47 \newblock 1990. |
|
48 |
|
49 \bibitem{devlin79} |
|
50 Keith~J. Devlin. |
|
51 \newblock {\em Fundamentals of Contemporary Set Theory}. |
|
52 \newblock Springer, 1979. |
32 |
53 |
33 \bibitem{dummett} |
54 \bibitem{dummett} |
34 Michael Dummett. |
55 Michael Dummett. |
35 \newblock {\em Elements of Intuitionism}. |
56 \newblock {\em Elements of Intuitionism}. |
36 \newblock Oxford University Press, 1977. |
57 \newblock Oxford University Press, 1977. |
37 |
58 |
38 \bibitem{dyckhoff} |
59 \bibitem{dyckhoff} |
39 Roy Dyckhoff. |
60 Roy Dyckhoff. |
40 \newblock Contraction-free sequent calculi for intuitionistic logic. |
61 \newblock Contraction-free sequent calculi for intuitionistic logic. |
41 \newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992. |
62 \newblock 57(3):795--807, 1992. |
42 |
63 |
43 \bibitem{felty91a} |
64 \bibitem{felty91a} |
44 Amy Felty. |
65 Amy Felty. |
45 \newblock A logic program for transforming sequent proofs to natural deduction |
66 \newblock A logic program for transforming sequent proofs to natural deduction |
46 proofs. |
67 proofs. |
49 \newblock LNAI 475. |
70 \newblock LNAI 475. |
50 |
71 |
51 \bibitem{frost93} |
72 \bibitem{frost93} |
52 Jacob Frost. |
73 Jacob Frost. |
53 \newblock A case study of co-induction in {Isabelle HOL}. |
74 \newblock A case study of co-induction in {Isabelle HOL}. |
54 \newblock Technical Report 308, University of Cambridge Computer Laboratory, |
75 \newblock Technical Report 308, August 1993. |
55 August 1993. |
|
56 |
|
57 \bibitem{OBJ} |
|
58 K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer. |
|
59 \newblock Principles of {OBJ2}. |
|
60 \newblock In {\em Symposium on Principles of Programming Languages}, pages |
|
61 52--66, 1985. |
|
62 |
76 |
63 \bibitem{gallier86} |
77 \bibitem{gallier86} |
64 J.~H. Gallier. |
78 J.~H. Gallier. |
65 \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem |
79 \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem |
66 Proving}. |
80 Proving}. |
67 \newblock Harper \& Row, 1986. |
81 \newblock Harper \& Row, 1986. |
68 |
82 |
69 \bibitem{mgordon88a} |
83 \bibitem{mgordon-hol} |
70 Michael J.~C. Gordon. |
84 M.~J.~C. Gordon and T.~F. Melham. |
71 \newblock {HOL}: A proof generating system for higher-order logic. |
85 \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher |
72 \newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI} |
86 Order Logic}. |
73 Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic |
87 \newblock 1993. |
74 Publishers, 1988. |
|
75 |
88 |
76 \bibitem{halmos60} |
89 \bibitem{halmos60} |
77 Paul~R. Halmos. |
90 Paul~R. Halmos. |
78 \newblock {\em Naive Set Theory}. |
91 \newblock {\em Naive Set Theory}. |
79 \newblock Van Nostrand, 1960. |
92 \newblock Van Nostrand, 1960. |
82 G.~P. Huet and B.~Lang. |
95 G.~P. Huet and B.~Lang. |
83 \newblock Proving and applying program transformations expressed with |
96 \newblock Proving and applying program transformations expressed with |
84 second-order patterns. |
97 second-order patterns. |
85 \newblock {\em Acta Informatica}, 11:31--55, 1978. |
98 \newblock {\em Acta Informatica}, 11:31--55, 1978. |
86 |
99 |
|
100 \bibitem{alf} |
|
101 Lena Magnusson and Bengt {Nordstr\"om}. |
|
102 \newblock The {ALF} proof editor and its proof engine. |
|
103 \newblock In {\em : International Workshop {TYPES '93}}, pages 213--237. |
|
104 Springer, published 1994. |
|
105 \newblock LNCS 806. |
|
106 |
87 \bibitem{mw81} |
107 \bibitem{mw81} |
88 Zohar Manna and Richard Waldinger. |
108 Zohar Manna and Richard Waldinger. |
89 \newblock Deductive synthesis of the unification algorithm. |
109 \newblock Deductive synthesis of the unification algorithm. |
90 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981. |
110 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981. |
91 |
111 |
92 \bibitem{martinlof84} |
112 \bibitem{martinlof84} |
93 Per Martin-L\"of. |
113 Per Martin-L\"of. |
94 \newblock {\em Intuitionistic type theory}. |
114 \newblock {\em Intuitionistic type theory}. |
95 \newblock Bibliopolis, 1984. |
115 \newblock Bibliopolis, 1984. |
96 |
116 |
|
117 \bibitem{melham89} |
|
118 Thomas~F. Melham. |
|
119 \newblock Automating recursive type definitions in higher order logic. |
|
120 \newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current |
|
121 Trends in Hardware Verification and Automated Theorem Proving}, pages |
|
122 341--386. Springer, 1989. |
|
123 |
97 \bibitem{milner-coind} |
124 \bibitem{milner-coind} |
98 Robin Milner and Mads Tofte. |
125 Robin Milner and Mads Tofte. |
99 \newblock Co-induction in relational semantics. |
126 \newblock Co-induction in relational semantics. |
100 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991. |
127 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991. |
101 |
128 |
102 \bibitem{noel} |
129 \bibitem{noel} |
103 Philippe {No\"el}. |
130 Philippe {No\"el}. |
104 \newblock Experimenting with {Isabelle} in {ZF} set theory. |
131 \newblock Experimenting with {Isabelle} in {ZF} set theory. |
105 \newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993. |
132 \newblock 10(1):15--58, 1993. |
106 |
133 |
107 \bibitem{nordstrom90} |
134 \bibitem{nordstrom90} |
108 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. |
135 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. |
109 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. |
136 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. |
110 \newblock Oxford University Press, 1990. |
137 \newblock Oxford University Press, 1990. |
113 Christine Paulin-Mohring. |
140 Christine Paulin-Mohring. |
114 \newblock Inductive definitions in the system {Coq}: Rules and properties. |
141 \newblock Inductive definitions in the system {Coq}: Rules and properties. |
115 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, |
142 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, |
116 December 1992. |
143 December 1992. |
117 |
144 |
118 \bibitem{paulson-set-I} |
|
119 Lawrence~C. Paulson. |
|
120 \newblock Set theory for verification: {I}. {From} foundations to functions. |
|
121 \newblock {\em Journal of Automated Reasoning}. |
|
122 \newblock In press; draft available as Report 271, University of Cambridge |
|
123 Computer Laboratory. |
|
124 |
|
125 \bibitem{paulson85} |
145 \bibitem{paulson85} |
126 Lawrence~C. Paulson. |
146 Lawrence~C. Paulson. |
127 \newblock Verifying the unification algorithm in {LCF}. |
147 \newblock Verifying the unification algorithm in {LCF}. |
128 \newblock {\em Science of Computer Programming}, 5:143--170, 1985. |
148 \newblock {\em Science of Computer Programming}, 5:143--170, 1985. |
129 |
149 |
130 \bibitem{paulson87} |
150 \bibitem{paulson87} |
131 Lawrence~C. Paulson. |
151 Lawrence~C. Paulson. |
132 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
152 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
133 \newblock Cambridge University Press, 1987. |
153 \newblock 1987. |
134 |
154 |
135 \bibitem{paulson-COLOG} |
155 \bibitem{paulson-COLOG} |
136 Lawrence~C. Paulson. |
156 Lawrence~C. Paulson. |
137 \newblock A formulation of the simple theory of types (for {Isabelle}). |
157 \newblock A formulation of the simple theory of types (for {Isabelle}). |
138 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
158 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
139 International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy |
159 International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy |
140 of Sciences, Springer. |
160 of Sciences, Springer. |
141 \newblock LNCS 417. |
161 \newblock LNCS 417. |
142 |
162 |
143 \bibitem{paulson91} |
|
144 Lawrence~C. Paulson. |
|
145 \newblock {\em {ML} for the Working Programmer}. |
|
146 \newblock Cambridge University Press, 1991. |
|
147 |
|
148 \bibitem{paulson-coind} |
163 \bibitem{paulson-coind} |
149 Lawrence~C. Paulson. |
164 Lawrence~C. Paulson. |
150 \newblock Co-induction and co-recursion in higher-order logic. |
165 \newblock Co-induction and co-recursion in higher-order logic. |
151 \newblock Technical Report 304, University of Cambridge Computer Laboratory, |
166 \newblock Technical Report 304, July 1993. |
152 July 1993. |
|
153 |
167 |
154 \bibitem{paulson-fixedpt} |
168 \bibitem{paulson-fixedpt} |
155 Lawrence~C. Paulson. |
169 Lawrence~C. Paulson. |
156 \newblock A fixedpoint approach to implementing (co-)inductive definitions. |
170 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
157 \newblock Technical report, University of Cambridge Computer Laboratory, 1993. |
171 \newblock Technical Report 320, December 1993. |
158 \newblock Draft. |
172 |
|
173 \bibitem{paulson-set-I} |
|
174 Lawrence~C. Paulson. |
|
175 \newblock Set theory for verification: {I}. {From} foundations to functions. |
|
176 \newblock 11(3):353--389, 1993. |
159 |
177 |
160 \bibitem{paulson-set-II} |
178 \bibitem{paulson-set-II} |
161 Lawrence~C. Paulson. |
179 Lawrence~C. Paulson. |
162 \newblock Set theory for verification: {II}. {Induction} and recursion. |
180 \newblock Set theory for verification: {II}. {Induction} and recursion. |
163 \newblock Technical Report 312, University of Cambridge Computer Laboratory, |
181 \newblock Technical Report 312, 1993. |
164 1993. |
182 |
|
183 \bibitem{paulson-final} |
|
184 Lawrence~C. Paulson. |
|
185 \newblock A concrete final coalgebra theorem for {ZF} set theory. |
|
186 \newblock Technical report, 1994. |
165 |
187 |
166 \bibitem{pelletier86} |
188 \bibitem{pelletier86} |
167 F.~J. Pelletier. |
189 F.~J. Pelletier. |
168 \newblock Seventy-five problems for testing automatic theorem provers. |
190 \newblock Seventy-five problems for testing automatic theorem provers. |
169 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. |
191 \newblock 2:191--216, 1986. |
170 \newblock Errata, JAR 4 (1988), 235--236. |
192 \newblock Errata, JAR 4 (1988), 235--236. |
171 |
193 |
172 \bibitem{plaisted90} |
194 \bibitem{plaisted90} |
173 David~A. Plaisted. |
195 David~A. Plaisted. |
174 \newblock A sequent-style model elimination strategy and a positive refinement. |
196 \newblock A sequent-style model elimination strategy and a positive refinement. |
175 \newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990. |
197 \newblock 6(4):389--402, 1990. |
176 |
198 |
177 \bibitem{quaife92} |
199 \bibitem{quaife92} |
178 Art Quaife. |
200 Art Quaife. |
179 \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory. |
201 \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory. |
180 \newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992. |
202 \newblock 8(1):91--147, 1992. |
181 |
203 |
182 \bibitem{suppes72} |
204 \bibitem{suppes72} |
183 Patrick Suppes. |
205 Patrick Suppes. |
184 \newblock {\em Axiomatic Set Theory}. |
206 \newblock {\em Axiomatic Set Theory}. |
185 \newblock Dover, 1972. |
207 \newblock Dover, 1972. |