{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:41:27Z","timestamp":1743104487358,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421962"},{"type":"electronic","value":"9783540453321"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45332-6_5","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T15:56:22Z","timestamp":1183478182000},"page":"117-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Scalable Certification for Typed Assembly Language"],"prefix":"10.1007","author":[{"given":"Dan","family":"Grossman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,13]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Twenty-Seventh ACM Symposium on Principles of Programming Languages, pages 243\u2013253, Boston, MA, January 2000.","DOI":"10.1145\/325694.325727"},{"key":"5_CR2","unstructured":"Quetzalcoatl Bradley, R. Nigel Horspool, and Jan Vitek. Jazz: An efficient compressed format for Java archive files. In CASCON\u201998, November 1998."},{"issue":"3","key":"5_CR3","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1145\/177492.177575","volume":"16","author":"P. Briggs","year":"1994","unstructured":"Preston Briggs, Keith Cooper, and Linda Torczon. Improvements to graph coloring register allocation. ACM Transactions on Progamming Languages and Systems, 16(3):428\u2013455, May 1994.","journal-title":"ACM Transactions on Progamming Languages and Systems"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0096-0551(81)90048-5","volume":"6","author":"G. Chaitin","year":"1981","unstructured":"G. Chaitin, M. Auslander, A. Chandra, J. Cocke, M. Hopkins, and P. Markstein. Register allocation via coloring. Computer Languages, 6:47\u201357, 1981.","journal-title":"Computer Languages"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Christopher Colby, Peter Lee, George Necula, and Fred Blau. A certifying compiler for Java. In ACM Conference on Programming Language Design and Implementation, pages 95\u2013107, Vancouver, Canada, 2000.","DOI":"10.1145\/358438.349315"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Karl Crary. A simple proof technique for certain parametricity results. In Fourth ACM International Conference on Functional Programming, pages 82\u201389, Paris, France, September 1999.","DOI":"10.1145\/317765.317787"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Jens Ernst, William Evans, Christopher W. Fraser, Todd A. Proebsting, and Steven Lucco. Code compression. In ACM Conference on Programming Language Design and Implementation, pages 358\u2013365, Las Vegas, NV, June 1997.","DOI":"10.1145\/258916.258947"},{"issue":"3","key":"5_CR8","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1145\/229542.229546","volume":"18","author":"L. George","year":"1996","unstructured":"Lal George and Andrew W. Appel. Iterated register coalescing. ACM Transactions on Progamming Languages and Systems, 18(3):300\u2013324, May 1996.","journal-title":"ACM Transactions on Progamming Languages and Systems"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Neal Glew. Type dispatch for named hierarchical types. In Fourth ACM International Conference on Functional Programming, pages 172\u2013182, Paris, France, September 1999.","DOI":"10.1145\/317765.317797"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Neal Glew and Greg Morrisett. Type safe linking and modular assembly language. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 250\u2013261, San Antonio, TX, January 1999.","DOI":"10.1145\/292540.292563"},{"issue":"1","key":"5_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for de ning logics. Journal of the ACM, 40(1):143\u2013184, 1993.","journal-title":"Journal of the ACM"},{"key":"5_CR12","unstructured":"Luke Hornof and Trevor Jim. Certifying compilation and run-time code generation. In ACM Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 60\u201374, San Antonio, TX, January 1999."},{"key":"5_CR13","unstructured":"David Kempe. Personal communication. Scalable Certi cation for Typed Assembly Language 145"},{"key":"5_CR14","unstructured":"Dexter Kozen. Efficient code certification. Technical Report 98-1661, Department of Computer Science, Cornell University, Ithaca, NY, January 1998."},{"key":"5_CR15","unstructured":"Xavier Leroy. The Objective Caml system, documentation, and user\u2019s guide, 1998."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Steven Lucco. Split-stream dictionary program compression. In ACM Conference on Programming Language Design and Implementation, pages 27\u201334, Vancouver, Canada, June 2000.","DOI":"10.1145\/358438.349307"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/0304-3975(92)90020-G","volume":"103","author":"H. Mairson","year":"1992","unstructured":"Harry Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387\u2013394, September 1992.","journal-title":"Theoretical Computer Science"},{"key":"5_CR18","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25\u201335, Atlanta, GA, 1999. Published as INRIA Technical Report 0288, March, 1999."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Workshop on Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28\u201352, Kyoto, Japan, March 1998. Springer-Verlag."},{"issue":"3","key":"5_CR20","first-page":"528","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Progamming Languages and Systems, 21(3):528\u2013569, May 1999.","journal-title":"ACM Transactions on Progamming Languages and Systems"},{"key":"5_CR21","series-title":"Technical Report","volume-title":"A notation for lambda terms II: Re nements and applications","author":"G. Nadathur","year":"1994","unstructured":"Gapolan Nadathur. A notation for lambda terms II: Re nements and applications. Technical Report CS-1994-01, Duke University, Durham, NC, January 1994."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation, pages 333\u2013344, Montreal, Canada, June 1998.","DOI":"10.1145\/277652.277752"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"George Necula and Peter Lee. Efficient representation and validation of proofs. In Thirteenth Symposium on Logic in Computer Science, pages 93\u2013104, Indianapolis, IN, June 1998.","DOI":"10.1109\/LICS.1998.705646"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"George Necula and S. P. Rahul. Oracle-based checking of untrusted software. In Twenty-Eigth ACM Symposium on Principles of Programming Languages, pages 142\u2013154, London, United Kingdom, January 2001.","DOI":"10.1145\/373243.360216"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"William Pugh. Compressing Java class files. In ACM Conference on Programming Language Design and Implementation, pages 247\u2013258, Atlanta, GA, May 1999.","DOI":"10.1145\/301631.301676"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Zhong Shao, Christopher League, and Stefan Monnier. Implementing typed intermediate languages. In Third ACM International Conference on Functional Programming, pages 313\u2013323, Baltimore, MD, September 1998.","DOI":"10.1145\/291251.289460"},{"key":"5_CR27","series-title":"Lect Notes Comput Sci","first-page":"366","volume-title":"Ninth European Symposium on Programming","author":"F. Smith","year":"2001","unstructured":"Fred Smith, David Walker, and Greg Morrisett. Alias types. In Ninth European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366\u2013381, Berlin, Germany, March 2000. Springer-Verlag."},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: a type-directed optimizing compiler for ML. In ACM Conference on Programming Language Design and Implementation, pages 181\u2013192, Philadelphia, PA, May 1996.","DOI":"10.1145\/249069.231414"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Philip Wadler. Theorems for free! In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 347\u2013359, London, United Kingdom, September 1989.","DOI":"10.1145\/99370.99404"},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/239912.239917","volume":"19","author":"A. K. Wright","year":"1997","unstructured":"Andrew K. Wright and Robert Cartwright. A practical soft type system for Scheme. ACM Transactions on Progamming Languages and Systems, 19(1):87\u2013152, January 1997.","journal-title":"ACM Transactions on Progamming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Types in Compilation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45332-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:02:02Z","timestamp":1737172922000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-45332-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421962","9783540453321"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45332-6_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"13 June 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}