163 \bibitem{paulson87} |
163 \bibitem{paulson87} |
164 Lawrence~C. Paulson. |
164 Lawrence~C. Paulson. |
165 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
165 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
166 \newblock Cambridge University Press, 1987. |
166 \newblock Cambridge University Press, 1987. |
167 |
167 |
168 \bibitem{paulson-COLOG} |
|
169 Lawrence~C. Paulson. |
|
170 \newblock A formulation of the simple theory of types (for {Isabelle}). |
|
171 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
|
172 International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy |
|
173 of Sciences, Springer. |
|
174 \newblock LNCS 417. |
|
175 |
|
176 \bibitem{paulson-coind} |
168 \bibitem{paulson-coind} |
177 Lawrence~C. Paulson. |
169 Lawrence~C. Paulson. |
178 \newblock Co-induction and co-recursion in higher-order logic. |
170 \newblock Co-induction and co-recursion in higher-order logic. |
179 \newblock Technical Report 304, Computer Laboratory, University of Cambridge, |
171 \newblock Technical Report 304, Computer Laboratory, University of Cambridge, |
180 July 1993. |
172 July 1993. |
199 |
191 |
200 \bibitem{paulson-CADE} |
192 \bibitem{paulson-CADE} |
201 Lawrence~C. Paulson. |
193 Lawrence~C. Paulson. |
202 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
194 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
203 \newblock In Alan Bundy, editor, {\em 12th International Conference on |
195 \newblock In Alan Bundy, editor, {\em 12th International Conference on |
204 Automated Deduction}, pages 148--161. Springer, 1994. |
196 Automated Deduction}, volume 814, pages 148--161. Springer, 1994. |
205 \newblock LNAI 814. |
197 |
|
198 \bibitem{paulson-COLOG} |
|
199 Lawrence~C. Paulson. |
|
200 \newblock A formulation of the simple theory of types (for {Isabelle}). |
|
201 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
|
202 International Conference on Computer Logic}, pages 246--274, Tallinn, |
|
203 Published 1990. Estonian Academy of Sciences, Springer. |
|
204 \newblock LNCS 417. |
206 |
205 |
207 \bibitem{pelletier86} |
206 \bibitem{pelletier86} |
208 F.~J. Pelletier. |
207 F.~J. Pelletier. |
209 \newblock Seventy-five problems for testing automatic theorem provers. |
208 \newblock Seventy-five problems for testing automatic theorem provers. |
210 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. |
209 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. |
226 \newblock Dover, 1972. |
225 \newblock Dover, 1972. |
227 |
226 |
228 \bibitem{takeuti87} |
227 \bibitem{takeuti87} |
229 G.~Takeuti. |
228 G.~Takeuti. |
230 \newblock {\em Proof Theory}. |
229 \newblock {\em Proof Theory}. |
231 \newblock North Holland, 2nd edition, 1987. |
230 \newblock North-Holland, 2nd edition, 1987. |
232 |
231 |
233 \bibitem{thompson91} |
232 \bibitem{thompson91} |
234 Simon Thompson. |
233 Simon Thompson. |
235 \newblock {\em Type Theory and Functional Programming}. |
234 \newblock {\em Type Theory and Functional Programming}. |
236 \newblock Addison-Wesley, 1991. |
235 \newblock Addison-Wesley, 1991. |