{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:58Z","timestamp":1725485578087},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_28","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:48:36Z","timestamp":1180651716000},"page":"418-434","source":"Crossref","is-referenced-by-count":2,"title":["Automating Type Soundness Proofs via Decision Procedures and Guided Reductions"],"prefix":"10.1007","author":[{"given":"Don","family":"Syme","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"28_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods In Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201. Springer-Verlag, November 1996. Palo Alto, California, November 6-8."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. A generalization of Shostak\u2019s method for combining decision procedures. In Frontiers of Combining Systems (FROCOS), Lecture Notes in Artificial Intelligence. Springer-Verlag, April 2002.","DOI":"10.1007\/3-540-45988-X_11"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Equality reasoning in sequent-based calculi. In Handbook of Automated Reasoning, Volume I, pages 611\u2013706. Elsevier Science and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"A. Gordon and D. Syme. Typing a multi-language intermediate code. In 27th Annual ACM Symposium on Principles of Programming Languages, January 2001.","DOI":"10.1145\/360204.360228"},{"key":"28_CR5","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":"28_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95","author":"J.G. Henriksen","year":"1995","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95, LNCS 1019, 1995."},{"key":"28_CR7","unstructured":"Xavier Leroy. The Objective Caml system, documentation and user\u2019s guide. INRIA, Rocquencourt, 1999. Available from http:\/\/caml. inria.fr ."},{"key":"28_CR8","unstructured":"Serge Lidin. Inside Microsoft.NET IL Assembler. Microsoft Press, 2002."},{"key":"28_CR9","unstructured":"Tobias Nipkow, David von Oheimb, and Cornelia Pusch. \u03bc Java: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Markto-berdorf 1999, pages 117\u2013144. IOS Press, 2000."},{"key":"28_CR10","unstructured":"M. Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998."},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201999","author":"C. Pusch","year":"1999","unstructured":"C. Pusch. Proving the soundness of a Java bytecode verifier specification in Is-abelle\/HOL. In TACAS\u201999, Lecture Notes in Computer Science. Springer Verlag, 1999."},{"key":"28_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48737-9_8","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1999","unstructured":"Z. Qian. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 271\u2013312. SpringerVerlag, 1999."},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Robert St\u00e4rk, Joachim Schmid, and Egon B\u00f6rger. Java and the Java Virtual Machine. Springer Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proceedings POPL\u201998, pages 149\u2013160. ACM Press, 1998.","DOI":"10.1145\/268946.268959"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"D. Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998.","DOI":"10.1007\/3-540-48256-3_14"},{"key":"28_CR16","unstructured":"M. VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania, May 1996."},{"key":"28_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"D. von Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 119\u2013156. Springer Verlag, 1999."},{"issue":"1","key":"28_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. K. Wright","year":"1994","unstructured":"Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38\u201394, 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:18:10Z","timestamp":1556450290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}