{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:13:20Z","timestamp":1778292800170,"version":"3.51.4"},"publisher-location":"London","reference-count":31,"publisher":"Springer London","isbn-type":[{"value":"9783540198840","type":"print"},{"value":"9781447134527","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/978-1-4471-3452-7_9","type":"book-chapter","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T07:13:53Z","timestamp":1335251633000},"page":"141-167","source":"Crossref","is-referenced-by-count":19,"title":["Z and HOL"],"prefix":"10.1007","author":[{"given":"Jonathan","family":"Bowen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Andrews PD. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Computer Science and Applied Mathematics Series. Academic Press, 1986."},{"key":"9_CR2","unstructured":"Boulton RJ, Gordon AD, Harrison JR, Herbert JMJ, Van Tassel J. Experience with embedding hardware description languages in HOL. In Stavridou V, Melham TF, Boute RT (eds), Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, IFIP Transactions A-10, pp 129\u2013156. North-Holland, 1992."},{"key":"9_CR3","first-page":"1994","volume-title":"Z User Workshop","author":"JP Bowen","year":"1994","unstructured":"Bowen JP. Comp.specification.z and Z FORUM frequently asked questions. In Bowen JP, Hall JA (eds), Z User Workshop, Cambridge 1994, Workshops in Computing. Springer-Verlag, 1994."},{"issue":"4","key":"9_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"JP Bowen","year":"1993","unstructured":"Bowen JP, Stavridou V. Safety-critical systems, formal methods and standards. IEE\/BCS Software Engineering Journal, 8 (4): 189\u2013209, 1993.","journal-title":"IEE\/BCS Software Engineering Journal"},{"key":"9_CR5","volume-title":"Accepted for ISO standardization","author":"SM Brien","year":"1992","unstructured":"Brien SM, Nicholls JE. Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory, UK, 1992. Accepted for ISO standardization, ISO\/IEC JTC1\/SC22."},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church A. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5: 56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"9_CR7","volume-title":"Fiddlers Green Lane","author":"RA Collinson","year":"1992","unstructured":"Collinson R. A simple demonstration of Balzac. Technical report, GCHQ, Fiddlers Green Lane, Cheltenham, Gloucestershire, UK, 1992."},{"key":"9_CR8","unstructured":"Diller A. Z: An Introduction to Formal Methods. Wiley, 1990."},{"key":"9_CR9","volume-title":"Cambridge University Press","author":"MJC Gordon","year":"1993","unstructured":"Gordon MJC, Melham TF (eds). Introduction to HOL: A Theorem-proving Environment for Higher-Order Logic. Cambridge University Press, 1993."},{"key":"9_CR10","volume-title":"Springer-Verlag","author":"MJC Gordon","year":"1979","unstructured":"Gordon MJC, Milner R, Wadsworth CP. Edinburgh LCF: A Mechanised Logic of Computation, vol 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"key":"9_CR11","volume-title":"Proof rules for Balzac. Technical Report WTH\/P7\/001","author":"WT Harwood","year":"1991","unstructured":"Harwood WT. Proof rules for Balzac. Technical Report WTH\/P7\/001, Imperial Software Technology, Cambridge, UK, 1991."},{"issue":"1","key":"9_CR12","first-page":"10","volume":"1","author":"RBICL Jones","year":"1992","unstructured":"Jones RB. ICL ProofPower. BCS FACS FACTS, Series III, 1 (1): 10\u201313, 1992.","journal-title":"Series III"},{"key":"9_CR13","volume-title":"Defence Research Agency, St. Andrews Road, Malvern, Worcestershire WR14","author":"R Macdonald","year":"1989","unstructured":"Macdonald R, Randell GP, Sennett CT. Pattern matching in ML: A case study in refinement. Report No. 89004, RSRE (now DRA), Defence Research Agency, St. Andrews Road, Malvern, Worcestershire WR14 3PS, UK, 1989."},{"key":"9_CR14","volume-title":"University of Edinburgh","author":"S Maharaj","year":"1990","unstructured":"Maharaj S. Implementing Z in LEGO. Master\u2019s thesis, University of Edinburgh, UK, 1990."},{"key":"9_CR15","unstructured":"Maharaj S. Encoding Z schemas in type theory. In Geuves H (ed), Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pp 209\u2013218, 1993. Distributed electronically."},{"key":"9_CR16","volume-title":"Woodcock JCP, Larsen PG (eds), FME93: Industrial-Strength Formal Methods, vol 670 of Lecture Notes in Computer Science, pp 462-481. Springer-Verlag","author":"A Martin","year":"1993","unstructured":"Martin A. Encoding W: A logic for Z in 2OBJ. In Woodcock JCP, Larsen PG (eds), FME\u201993: Industrial-Strength Formal Methods, vol 670 of Lecture Notes in Computer Science, pp 462\u2013481. Springer-Verlag, 1993."},{"key":"9_CR17","volume-title":"Milne GJ (ed), The Fusion of Hardware Design and Verification, Proceedings of the IFIP WG10.2 Working Conference, pp 27-50. North-Holland","author":"T Melham","year":"1988","unstructured":"Melham T. Using recursive types to reason about hardware in Higher Order Logic. In Milne GJ (ed), The Fusion of Hardware Design and Verification, Proceedings of the IFIP WG10.2 Working Conference, pp 27\u201350. North-Holland, 1988."},{"key":"9_CR18","volume-title":"The MIT Press","author":"R Milner","year":"1990","unstructured":"Milner R, Tofte M, Harper R. The Definition of Standard ML. The MIT Press, 1990."},{"key":"9_CR19","volume-title":"Nicholls JE (ed), Z User Workshop, Oxford 1990, Workshops in Computing, pp 105-128. Springer-Verlag","author":"D Neilson","year":"1991","unstructured":"Neilson D. Machine support for Z: the zedB tool. In Nicholls JE (ed), Z User Workshop, Oxford 1990, Workshops in Computing, pp 105\u2013128. Springer-Verlag, 1991."},{"key":"9_CR20","volume-title":"Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 243-258. Springer-Verlag","author":"D Neilson","year":"1992","unstructured":"Neilson D, Prasad D. zedB: A proof tool for Z built on B. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 243\u2013258. Springer-Verlag, 1992."},{"key":"9_CR21","volume-title":"Cambridge University Press","author":"LC Logic","year":"1987","unstructured":"Paulson LC. Logic and Computation: Interactive Proof with Cambridge LCF, vol 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987."},{"key":"9_CR22","volume-title":"fixedpoint approach to implementing (co-)inductive definitions. Technical report, University of Cambridge","author":"LCA Paulson","year":"1993","unstructured":"Paulson LC. A fixedpoint approach to implementing (co-)inductive definitions. Technical report, University of Cambridge, Computer Laboratory, UK, 1993. Draft."},{"key":"9_CR23","volume-title":"Prentice Hall International Series in Computer Science","author":"BF Potter","year":"1990","unstructured":"Potter BF, Sinclair JE, Till D. An Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science, 1990."},{"key":"9_CR24","volume-title":"Canada","author":"MZ Saaltink","year":"1991","unstructured":"Saaltink M. Z and EVES. Technical Report TR\u201391\u20135449\u201302, Odyyssey Research Associates, 265 Carling Avenue, Suite 506, Ottawa, Ontario K1S 2E1, Canada, 1991."},{"key":"9_CR25","volume-title":"Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 223-242. Springer-Verlag","author":"M Saaltink","year":"1992","unstructured":"Saaltink M. Z and Eves. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 223\u2013242. Springer-Verlag, 1992."},{"key":"9_CR26","volume-title":"Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 3-39. Springer-Verlag","author":"A Smith","year":"1992","unstructured":"Smith A. On recursive free types in Z. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 3\u201339. Springer-Verlag, 1992."},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1049\/sej.1989.0006","volume":"4","author":"JM Spivey","year":"1989","unstructured":"Spivey JM. An introduction to Z and formal specifications. IEE\/BCS Software Engineering Journal, 4 (1): 40\u201350, 1989.","journal-title":"IEE\/BCS Software Engineering Journal"},{"key":"9_CR28","volume-title":"Oxford OX9 9AN, UK","author":"JM Spivey","year":"1992","unstructured":"Spivey JM. The fuzz Manual. Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9 9AN, UK, 2nd edition, 1992."},{"key":"9_CR29","volume-title":"Prentice Hall International Series in Computer Science","author":"JM Spivey","year":"1992","unstructured":"Spivey JM. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992."},{"key":"9_CR30","volume-title":"Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 77-96. Springer-Verlag","author":"JCP Woodcock","year":"1992","unstructured":"Woodcock JCP, Brien SM. W: A logic for Z. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 77\u201396. Springer-Verlag, 1992."},{"key":"9_CR31","unstructured":"Xiaoping Jia. ZTC: A Type Checker for Z User\u2019s Guide. Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University, Chicago, IL 60604, USA (e-mail: j is@cs. depaul. edu), 1994."}],"container-title":["Workshops in Computing","Z User Workshop, Cambridge 1994"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3452-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T23:49:55Z","timestamp":1557964195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-3452-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540198840","9781447134527"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3452-7_9","relation":{},"ISSN":["1431-1682"],"issn-type":[{"value":"1431-1682","type":"print"}],"subject":[],"published":{"date-parts":[[1994]]}}}