{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:49:17Z","timestamp":1770295757508,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_11","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"149-165","source":"Crossref","is-referenced-by-count":69,"title":["Locales A Sectioning Concept for Isabelle"],"prefix":"10.1007","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Wenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"11_CR1","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, and C. Mu\u00f1oz. The Coq Proof Assistant User\u2019s Guide, version 6.1. INRIARocquencourt et CNRS-ENS Lyon, 1996."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, pages 56\u201368, 1940.","DOI":"10.2307\/2266170"},{"key":"11_CR3","unstructured":"K. Mani Chandi and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988."},{"key":"11_CR4","unstructured":"N. G. de Bruijn. A Survey of the Project AUTOMATH. In J.P. Seldin and J.R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Academic Press Limited, pages 579\u2013606. 1980."},{"key":"11_CR5","unstructured":"G. Dowek. Naming and Scoping in a Mathematical Vernacular. Technical Report 1283, INRIA, Rocquencourt, 1990."},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"John V. Guttag and James J. Horning, editors. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993. With Stephen J. Garland, Kevin D. Jones, Andr\u00e9s Modet, and Jeannette M. Wing.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"11_CR8","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"F. Kamm\u00fcller. Modular Reasoning in Isabelle. PhD thesis, University of Cambridge, 1999. submitted.","DOI":"10.1007\/10721959_7"},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs: TYPES\u2019 98","author":"F. Kamm\u00fcller","year":"1999","unstructured":"F. Kamm\u00fcller. Modular Structures as Dependent Types in Isabelle. In Types for Proofs and Programs: TYPES\u2019 98, LNCS. Springer-Verlag, 1999. Selected papers. To appear."},{"key":"11_CR11","unstructured":"F. Kamm\u00fcller and L. C. Paulson. A Formal Proof of Sylow\u2019s First Theorem \u2014 An Experiment in Abstract Algebra with Isabelle HOL. Journal of Automated Reasoning, 1999. To appear."},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","volume-title":"11th International Conference on Theorem Proving in Higher Order Logics","author":"W. Naraschewski","year":"1998","unstructured":"W. Naraschewski and M. Wenzel. Object-oriented Verification based on Record Subtyping in Higher-Order Logic. In 11th International Conference on Theorem Proving in Higher Order Logics, volume 1479 of LNCS, ANU, Canberra, Australia, 1998. Springer-Verlag."},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"O.R.R.+.9.6._.S. Owre","year":"1996","unstructured":"[ORR+96]_S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification, volume 1102 of LNCS. Springer, 1996."},{"key":"11_CR14","unstructured":"S. Owre, N. Shankar, J.M. Rushby, and D.W.J. Stringer-Calvert. PVS Language Reference. Part of the PVS Manual. Available on the Web as http:\/\/www.csl.sri.com\/pvsweb\/manuals.html , September 1998."},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"P. J. Windley. Abstract Theories in HOL. In L. Claesen and M. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, IFIP Transactions A-20, pages 197\u2013210. North-Holland, 1993.","DOI":"10.1016\/B978-0-444-89880-7.50019-X"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T13:46:42Z","timestamp":1683985602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}