{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:58:01Z","timestamp":1770994681913,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540430025","type":"print"},{"value":"9783540452942","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45294-x_13","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T22:45:12Z","timestamp":1181601912000},"page":"144-155","source":"Crossref","is-referenced-by-count":10,"title":["A Mechanically Verified Compiling Specification for a Lisp Compiler"],"prefix":"10.1007","author":[{"given":"Axel","family":"Dold","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Vialard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,26]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation","author":"E. B\u00f6rger","year":"1998","unstructured":"E. B\u00f6rger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd Int. Symposium on Mathematical Foundations of Computer Science, volume 1450 of LNCS. Springer, 1998."},{"key":"13_CR2","unstructured":"M. Broy. Experiences with Software Specification and Verification using LP, the Larch Proof Assistant. Technical report, Digital Systems Research Center, 1992."},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/5397.30847","volume":"8","author":"L.M. Chirica","year":"1986","unstructured":"L.M. Chirica and D.F. Martin. Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Languages and Systems, 8(2):185\u2013214, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR4","unstructured":"Paul Curzon. The Verified Compilation of Vista Programs. Internal Report, Computer Laboratory, University of Cambridge, January 1994."},{"key":"13_CR5","volume-title":"Formal Software Development using Generic Development Steps","author":"A. Dold","year":"2000","unstructured":"Axel Dold. Formal Software Development using Generic Development Steps. Logos-Verlag, Berlin, 2000. Dissertation, Universit\u00e4t Ulm."},{"key":"13_CR6","unstructured":"W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler Correctness and Implementation Verification: The Verifix Approach. In Proceedings of the Poster Session of CC\u201996-International Conference on Compiler Construction. ida, 1996. TR-Nr.: R-96-12."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Wolfgang Goerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS\u201998 Workshop on \u201cTool Support for System Specification, Development, and Verification\u201d, Advances in Computing Science, Malente, 1998. Springer Verlag.","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"13_CR8","unstructured":"Wolfgang Goerigk and H. Langmaack. Compiler Implementation Verification and Trojan Horses. In D. Bainov, editor, Proc. of the 9th Int. Colloquium on Numerical Analysis and Computer Sciences with Applications, Plovdiv, Bulgaria, 2000."},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-48092-7_10","volume-title":"Correct System Design","author":"G. Goos","year":"1999","unstructured":"G. Goos and W. Zimmermann. Verification of Compilers. In B. Steffen E.-R. Olderog, editor, Correct System Design, volume 1710 of LNCS, pages 201\u2013230. Springer-Verlag, 1999."},{"key":"13_CR10","series-title":"Technical Report","volume-title":"A Guide to VLISP, A Verified Programming Language Implementation","author":"J. D. Guttman","year":"1992","unstructured":"J. D. Guttman, L. G. Monk, J. D. Ramsdell, W. M. Farmer, and V. Swarup. A Guide to VLISP, A Verified Programming Language Implementation. Technical Report M92B091, The MITRE Corporation, Bedford, MA, September 1992."},{"key":"13_CR11","unstructured":"Ulrich Hoffmann. Compiler Implementation Verification through Rigorous Syntactical Code Inspection. PhD thesis, Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t zu Kiel, Kiel, 1998."},{"key":"13_CR12","series-title":"Technical Report","volume-title":"A Verified Compiler for a Verified Microprocessor","author":"J.J. Joyce","year":"1989","unstructured":"J.J. Joyce. A Verified Compiler for a Verified Microprocessor. Technical Report 167, University of Cambridge, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England, March 1989."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"J. McCarthy and J.A. Painter. Correctness of a Compiler for Arithmetical Expressions. In J.T. Schwartz, editor, Proceedings of a Symposium in Applied Mathematics, 19, Mathematical Aspects of Computer Science. American Mathematical Society, 1967.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"J S. Moore. A Mechanically Verified Language Implementation. Journal of Automated Reasoning, 5(4), 1989.","DOI":"10.1007\/BF00243133"},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"Markus M\u00fcller-Olm. Modular Compiler Verification, volume 1283 of LNCS. Springer Verlag, Berlin, Heidelberg, New York, 1997. PhD Thesis."},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10886-6","volume-title":"Compiler Specification and Verification","author":"W. Polak","year":"1981","unstructured":"W. Polak. Compiler Specification and Verification, volume 124 of LNCS. Springer-Verlag, 1981."},{"key":"13_CR18","unstructured":"Gerhard Schellhorn. Verifikation abstrakter Zustandsmaschinen. PhD thesis, Unversit\u00e4t Ulm, 1999."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45294-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T21:28:08Z","timestamp":1556486888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45294-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430025","9783540452942"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45294-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}