{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:27:18Z","timestamp":1725492438879},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665373"},{"type":"electronic","value":"9783540481676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48167-2_9","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T07:40:19Z","timestamp":1191570019000},"page":"121-133","source":"Crossref","is-referenced-by-count":3,"title":["Modular Structures as Dependent Types in Isabelle"],"prefix":"10.1007","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"9_CR1","unstructured":"R. Burstall. Computer Assisted Proof for Mathematics: an Introduction using the LEGO Proof System. Technical Report ECS-LFCS-91-132, University of Edinburgh, 1990. 131"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, pages 56\u201368, 1940. 125","DOI":"10.2307\/2266170"},{"key":"9_CR3","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. 121, 122, 123","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR4","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. 121, 123","DOI":"10.1007\/978-1-4612-2704-5_7"},{"key":"9_CR5","unstructured":"A. Heyting. Intuitionism: An Introduction. North Holland, Amsterdam, 1956. 125"},{"key":"9_CR6","unstructured":"F. Kamm\u00fcller and L. C. Paulson. A Formal Proof of Sylow\u2019s First Theorem-An Experiment in Abstract Algebra with Isabelle HOL. Journal of Automated Reasoning, 1999. To appear. 121"},{"key":"9_CR7","unstructured":"F. Kamm\u00fcller and M. Wenzel. Locales-a Sectioning Concept for Isabelle. Technical Report 449, University of Cambridge, Computer Laboratory, 1998. 131"},{"key":"9_CR8","unstructured":"Z. Luo and R. Pollack. Lego proof development system: User\u2019s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992. 131"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Z. Luo. A Higher-order Calculus and Theory Abstraction. Information and Computation, 90(1), 1990. 131","DOI":"10.1016\/0890-5401(91)90062-7"},{"key":"9_CR10","unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90. 131"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"D. B. MacQueen. Using Dependant Types to Express Modular Structures. In Proc. 13th ACM Symp. Principles Programming Languages. ACM Press, 1986. 131","DOI":"10.1145\/512644.512670"},{"key":"9_CR12","volume-title":"Oxford Science Publications","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f\u2019 s Type Theory \u2014 An Introduction. Oxford Science Publications. Clarendon Press, Oxford, 1990. 125"},{"key":"9_CR13","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. 121, 123"},{"key":"9_CR14","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language (Beta Release). Technical report, SRI International, 1993. 121, 123"},{"key":"9_CR15","unstructured":"R. Pollack. The Tarski Fixpoint Theorem. http:\/\/e-mail to: proof-sci@se.chalmers.cs , 1990. 131"},{"key":"9_CR16","unstructured":"R. Pollack. Theories in Type Theory. Slides, available on the Web as http:\/\/www.brics.dk\/pollack , unknown year. 132"},{"key":"9_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-12727-5_24","volume-title":"CAAP\u201983: Trees in Algebra and Programming","author":"D. T. Sannella","year":"1983","unstructured":"D. T. Sannella and R. M. Burstall. Structured Theories in LCF. In CAAP\u201983: Trees in Algebra and Programming, volume 159 of LNCS, pages 377\u201391. Springer-Verlag, 1983. 131"},{"key":"9_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285\u2013309, 1955. 130","journal-title":"Pacific Journal of Mathematics"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48167-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T15:06:24Z","timestamp":1556895984000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48167-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665373","9783540481676"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48167-2_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}