{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:13Z","timestamp":1725474493840},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097791","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"154-172","source":"Crossref","is-referenced-by-count":16,"title":["Proof style"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"9_CR1","unstructured":"Back, R., Grundy, J., and von Wright, J. (1996) Structured calculational proof. Technical Report 65, Turku Centre for Computer Science (TUCS), Lemmink\u00e4isenkatu 14 A, FIN-20520 Turku, Finland. Also available as Technical Report TR-CS-96-09 from the Australian National University."},{"key":"9_CR2","unstructured":"Boyer, R. S. and Moore, J S. (1979) A Computational Logic. ACM Monograph Series. Academic Press."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"de Bruijn, N. G. (1970) The mathematical language AUTOMATH, its usage and some of its extensions. In Laudet, M., Lacombe, D., Nolin, L., and Sch\u00fctzenberger, M. (eds.), Symposium on Automatic Demonstration, Volume 125 of Lecture Notes in Mathematics, pp. 29\u201361. Springer-Verlag.","DOI":"10.1007\/BFb0060623"},{"key":"9_CR4","unstructured":"Chen, W. (1992) Tactic-based theorem proving and knowledge-based forward chaining. See Kapur (1992), pp. 552\u2013566."},{"key":"9_CR5","unstructured":"Cohn, A. (1990) Proof accounts in HOL (incomplete draft). Available on the Web as http:\/\/www.cl.cam.ac.uk\/users\/mjcg\/AccountsPaper.ps.gz."},{"key":"9_CR6","unstructured":"Constable, R. (1986) Implementing Mathematics with The Nuprl Proof Development System. Prentice-Hall."},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BF00244273","volume":"1","author":"R. L. Constable","year":"1985","unstructured":"Constable, R. L., Knoblock, T. B., and Bates, J. L. (1985) Writing programs that construct proofs. Journal of Automated Reasoning, 1, 285\u2013326.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Coscoy, Y., Kahn, G., and Th\u00e9ry, L. (1995) Extracting text from proofs. In Dezani-Ciancaglini, M. and Plotkin, G. (eds.), Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, Volume 902 of Lecture Notes in Computer Science, Edinburgh, pp. 109\u2013123. Springer-Verlag.","DOI":"10.1007\/BFb0014048"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1093\/comjnl\/38.2.91","volume":"38","author":"P. Curzon","year":"1995","unstructured":"Curzon, P. (1995) Tracking design changes with formal machine-checked proof. The Computer Journal, 38, 91\u2013100.","journal-title":"The Computer Journal"},{"key":"9_CR10","unstructured":"Garland, S. J. and Guttag, J. V. (1991) A guide to LP, the Larch Prover. Technical report, MIT Laboratory for Computer Science."},{"key":"9_CR11","first-page":"462","volume-title":"Proceedings of the 8th international conference on computer aided verification (CAV'96), Volume 1102 of Lecture Notes in Computer Science","author":"G. Gonthier","year":"1996","unstructured":"Gonthier, G. (1996) Verifying the safety of a practical concurrent garbage collector. In Alur, R. and Henzinger, T. A. (eds.), Proceedings of the 8th international conference on computer aided verification (CAV'96), Volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, pp. 462\u2013465. Springer-Verlag."},{"key":"9_CR12","unstructured":"Gordon, M. J. C. and Melham, T. F. (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Gordon, M. J. C., Milner, R., and Wadsworth, C. P. (1979) Edinburgh LCF: A Mechanised Logic of Computation, Volume 78 of Lecture Notes in Computer Science. Springer-Verlag.","DOI":"10.1007\/3-540-09724-4"},{"key":"9_CR14","unstructured":"Grundy, J. (1996) A browsable format for proof presentation. In Gefwert, C., Orponen, P., and Sepp\u00e4nen, J. (eds.), Proceedings of the Finnish Artificial Intelligence Society Symposium: Logic, Mathematics and the Computer, Volume 14 of Suomen Teko\u00e4lyseuran julkaisuja, pp. 171\u2013178. Finnish Artificial Intelligence Society."},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J. R. Guard","year":"1969","unstructured":"Guard, J. R., Oglesby, F. C., Bennett, J. H., and Settle, L. G. (1969) Semiautomated mathematics. Journal of the ACM, 16, 49\u201362.","journal-title":"Journal of the ACM"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Harrison, J. (1996) A Mizar mode for HOL. In von Wright, J., Grundy, J., and Harrison, J. (eds.), Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland, pp. 203\u2013220. Springer-Verlag.","DOI":"10.1007\/BFb0105406"},{"key":"9_CR17","unstructured":"van Bentham Jutting, L. S. (1977) Checking Landau's \u201cGrundlagen\u201d in the AUTOMATH System. Ph. D. thesis, Eindhoven University of Technology. Useful summary in Nederpelt, Geuvers, and de Vrijer (1994), pp. 701\u2013732."},{"volume-title":"11th International Conference on Automated Deduction, Volume 607 of Lecture Notes in Computer Science","year":"1992","key":"9_CR18","unstructured":"Kapur, D. (ed.) (1992) 11th International Conference on Automated Deduction, Volume 607 of Lecture Notes in Computer Science, Saratoga, NY. Springer-Verlag."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Kreisel, G. (1985) Proof theory and the synthesis of programs: Potential and limitations. In Buchberger, B. (ed.), EUROCAL '85: European Conference on Computer Algebra, Volume 203 of Lecture Notes in Computer Science, pp. 136\u2013150. Springer-Verlag.","DOI":"10.1007\/3-540-15983-5_12"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/BF03023977","volume":"12","author":"C. W. H. Lam","year":"1990","unstructured":"Lam, C. W. H. (1990) How reliable is a computer-based proof? The Mathematical Intelligencer, 12, 8\u201312.","journal-title":"The Mathematical Intelligencer"},{"key":"9_CR21","series-title":"Research Report","volume-title":"How to write a proof","author":"L. Lamport","year":"1993","unstructured":"Lamport, L. (1993) How to write a proof. Research Report 94, DEC Systems Research Center, 130 Lytton Avenue, Palo Alto, California 94301, USA."},{"key":"9_CR22","unstructured":"Landau, E. (1930) Grundlagen der Analysis. Leipzig. English translation by F. Steinhardt: \u201cFoundations of analysis: the arithmetic of whole, rational, irrational, and complex numbers. A supplement to textbooks on the differential and integral calculus', published by Chelsea; 3rd edition 1966."},{"key":"9_CR23","unstructured":"McAllester, D. A. (1989) ONTIC: A Knowledge Representation System for Mathematics. MIT Press."},{"key":"9_CR24","unstructured":"Nederpelt, R. P., Geuvers, J. H., and de Vrijer, R. C. (eds.) (1994) Selected Papers on Automath, Volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland."},{"key":"9_CR25","unstructured":"Owre, S., Rushby, J. M., and Shankar, N. (1992) PVS: A prototype verification system. See Kapur (1992), pp. 748\u2013752."},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. (1987) Logic and computation: interactive proof with Cambridge LCF, Volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.","DOI":"10.1017\/CBO9780511526602"},{"key":"9_CR27","unstructured":"Paulson, L. C. (1990) Isabelle: The next 700 theorem provers. In Odifreddi, P. G. (ed.), Logic and Computer Science, Volume 31 of APIC Studies in Data Processing, pp. 361\u2013386. Academic Press."},{"key":"9_CR28","unstructured":"Paulson, L. C. (1994) Isabelle: a generic theorem prover, Volume 828 of Lecture Notes in Computer Science. Springer-Verlag. With contributions by Tobias Nipkow."},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"L. C. Paulson","year":"1996","unstructured":"Paulson, L. C. and Gr\u0105bczewski, K. (1996) Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17, 291\u2013323.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Pollack, R. (1995) On extensibility of proof checkers. In Dybjer, P., Nordstr\u00f6m, B., and Smith, J. (eds.), Types for Proofs and Programs: selected papers from TYPES'94, Volume 996 of Lecture Notes in Computer Science, B\u00e5stad, pp. 140\u2013161. Springer-Verlag.","DOI":"10.1007\/3-540-60579-7_8"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Prasetya, I. S. W. B. (1993) On the style of mechanical proving. In Joyce, J. J. and Seger, C. (eds.), Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, Volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, pp. 475\u2013488. Springer-Verlag.","DOI":"10.1007\/3-540-57826-9_157"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Robinson, J. A. (1994) Logic, computers, Turing and von Neumann. In Furukawa, K., Michie, D., and Muggleton, S. (eds.), Machine Intelligence 13, pp. 1\u201335. Clarendon Press.","DOI":"10.1093\/oso\/9780198538509.003.0001"},{"key":"9_CR33","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"Rudnicki, P. (1987) Obvious inferences. Journal of Automated Reasoning, 3, 383\u2013393.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR34","unstructured":"Rudnicki, P. (1992) An overview of the MIZAR project. Available by anonymous FTP from menaik.cs.ualberta.ca as pub\/Mizar\/Mizar_Over.tar.Z."},{"key":"9_CR35","series-title":"Technical Report","volume-title":"DECLARE: A prototype declarative proof system for higher order logic","author":"D. Syme","year":"1997","unstructured":"Syme, D. (1997a) DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK."},{"key":"9_CR36","series-title":"Technical Report","volume-title":"Proving Java type soundness","author":"D. Syme","year":"1997","unstructured":"Syme, D. (1997b) Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK."},{"key":"9_CR37","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Trybulec, A. (1978) The Mizar-QC\/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing), 6, 136\u2013140.","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Trybulec, A. and Blair, H. A. (1985) Computer aided reasoning. In Parikh, R. (ed.), Logics of Programs, Volume 193 of Lecture Notes in Computer Science, Brooklyn, pp. 406\u2013412. Springer-Verlag.","DOI":"10.1007\/3-540-15648-8_30"},{"key":"9_CR39","first-page":"103","volume":"10\/11","author":"Z. Trybulec","year":"1991","unstructured":"Trybulec, Z. and \u015awi\u0119czkowska, H. (1991-1992) The language of mathematical texts. Studies in Logic, Grammar and Rhetoric, Biakystok, 10\/11, 103\u2013124.","journal-title":"Studies in Logic, Grammar and Rhetoric, Biakystok"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097791","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T14:07:15Z","timestamp":1707401235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097791"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/bfb0097791","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}