{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:33:27Z","timestamp":1750307607476,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T00:00:00Z","timestamp":1263859200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,19]]},"DOI":"10.1145\/1707790.1707793","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T20:15:04Z","timestamp":1263932104000},"page":"9-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Operating system development with ATS"],"prefix":"10.1145","author":[{"given":"Matthew","family":"Danish","sequence":"first","affiliation":[{"name":"Boston University, Boston, MA, USA"}]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[{"name":"Boston University, Boston, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2010,1,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_2_1_2_1","unstructured":"Fabrice Bellard et al. QEMU: machine emulator. http:\/\/www.qemu.org\/ 2009.  Fabrice Bellard et al. QEMU: machine emulator. http:\/\/www.qemu.org\/ 2009."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224077"},{"key":"e_1_3_2_1_4_1","unstructured":"Matthias Blume et al. Standard ML of New Jersey. http:\/\/www.smlnj.org\/ 2009.  Matthias Blume et al. Standard ML of New Jersey. http:\/\/www.smlnj.org\/ 2009."},{"key":"e_1_3_2_1_5_1","volume-title":"Modula-3 report (revised). Technical report","author":"Luca Cardelli","year":"1989","unstructured":"Luca Cardelli et al. Modula-3 report (revised). Technical report , Digital Equipment Corp. (now HP Inc .), Nov 1989 . http:\/\/www.hpl.hp.com\/techreports\/Compaq-DEC\/SRC-RR-52.html. Luca Cardelli et al. Modula-3 report (revised). Technical report, Digital Equipment Corp. (now HP Inc.), Nov 1989. http:\/\/www.hpl.hp.com\/techreports\/Compaq-DEC\/SRC-RR-52.html."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/978-3-540-71316-6_35","volume-title":"Programming Languages and Systems","author":"Condit Jeremy","year":"2007","unstructured":"Jeremy Condit , Matthew Harren , Zachary Anderson , David Gay , and George C. Necula . Programming Languages and Systems , chapter Dependent Types for Low-level Programming, pages 520 -- 535 . Lecture Notes in Computer Science. Springer Berlin \/ Heidelberg , 2007 . Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. Programming Languages and Systems, chapter Dependent Types for Low-level Programming, pages 520--535. Lecture Notes in Computer Science. Springer Berlin \/ Heidelberg, 2007."},{"key":"e_1_3_2_1_7_1","unstructured":"Bryce Denny Christophe Bothamy Donald Becker etal BOCHS: x86 PC emulator. http:\/\/bochs.sourceforge.net\/ 2009.  Bryce Denny Christophe Bothamy Donald Becker et al. BOCHS: x86 PC emulator. http:\/\/bochs.sourceforge.net\/ 2009."},{"key":"e_1_3_2_1_8_1","volume-title":"Design and Implementation of an Operating System in Standard ML. Master's thesis","author":"Fu Guangrui","year":"1999","unstructured":"Guangrui Fu . Design and Implementation of an Operating System in Standard ML. Master's thesis , University of Hawaii , Aug 1999 . http:\/\/www2.hawaii.edu\/esb\/prof\/proj\/hello\/. Guangrui Fu. Design and Implementation of an Operating System in Standard ML. Master's thesis, University of Hawaii, Aug 1999. http:\/\/www2.hawaii.edu\/esb\/prof\/proj\/hello\/."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1090189.1086380"},{"key":"e_1_3_2_1_10_1","unstructured":"Hugo Herbelin. Coq proof assistant. http:\/\/coq.inria.fr\/ 2009.  Hugo Herbelin. Coq proof assistant. http:\/\/coq.inria.fr\/ 2009."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, 2005","author":"Hohmuth M.","year":"2005","unstructured":"M. Hohmuth and H. Tews . The VFiasco approach for a verified operating system . In Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, 2005 . http:\/\/www.cs.ru.nl\/H.Tews\/Plos- 2005 \/ecoop-plos-05-letter.pdf. M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, 2005. http:\/\/www.cs.ru.nl\/H.Tews\/Plos-2005\/ecoop-plos-05-letter.pdf."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243424"},{"key":"e_1_3_2_1_13_1","unstructured":"Intel Inc. Intel\u2122 64 and IA-32 Architectures Software Developer's Manuals. http:\/\/www.intel.com\/products\/processor\/manuals\/.  Intel Inc. Intel\u2122 64 and IA-32 Architectures Software Developer's Manuals. http:\/\/www.intel.com\/products\/processor\/manuals\/."},{"key":"e_1_3_2_1_14_1","unstructured":"VMWare Inc. VMWare: Virtual Machine software. http:\/\/www.vmware.com\/ 2009.  VMWare Inc. VMWare: Virtual Machine software. http:\/\/www.vmware.com\/ 2009."},{"key":"e_1_3_2_1_15_1","first-page":"275","volume-title":"Yanling Wang. Cyclone: A Safe Dialect of C. In ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , and Yanling Wang. Cyclone: A Safe Dialect of C. In ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference , pages 275 -- 288 , Berkeley, CA, USA , 2002 . USENIX Association. Trevor Jim, J. Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. Cyclone: A Safe Dialect of C. In ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, pages 275--288, Berkeley, CA, USA, 2002. USENIX Association."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/365628.365655"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/234215.234473"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"e_1_3_2_1_21_1","unstructured":"Larry Paulson and Tobias Nipkow. Isabelle proof assistant. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/ 2009.  Larry Paulson and Tobias Nipkow. Isabelle proof assistant. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/ 2009."},{"key":"e_1_3_2_1_22_1","unstructured":"Simon Peyton-Jones Simon Marlow etal The Glasgow Haskell Compiler. http:\/\/www.haskell.org\/ghc\/ 2009.  Simon Peyton-Jones Simon Marlow et al. The Glasgow Haskell Compiler. http:\/\/www.haskell.org\/ghc\/ 2009."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292605"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_21"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481856"},{"key":"e_1_3_2_1_26_1","unstructured":"Richard West. The Quest operating system. http:\/\/www.cs.bu.edu\/fac\/richwest\/quest 2009.  Richard West. The Quest operating system. http:\/\/www.cs.bu.edu\/fac\/richwest\/quest 2009."},{"key":"e_1_3_2_1_27_1","first-page":"394","volume-title":"Post-workshop Proceedings of TYPES 2003","author":"Xi Hongwei","year":"2004","unstructured":"Hongwei Xi . Applied Type System (extended abstract) . In Post-workshop Proceedings of TYPES 2003 , pages 394 -- 408 , 2004 . Hongwei Xi. Applied Type System (extended abstract). In Post-workshop Proceedings of TYPES 2003, pages 394--408, 2004."},{"key":"e_1_3_2_1_28_1","unstructured":"Hongwei Xi. ATS\/LF: a type system for constructing proofs as total functional programs. http:\/\/www.ats-lang.org\/PAPER\/ATSLF-PAfestschrift.pdf 2004.  Hongwei Xi. ATS\/LF: a type system for constructing proofs as total functional programs. http:\/\/www.ats-lang.org\/PAPER\/ATSLF-PAfestschrift.pdf 2004."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_3_2_1_30_1","unstructured":"Hongwei Xi. Examples encoding deduction systems. http:\/\/www.ats-lang.org\/EXAMPLE\/LF\/LF.html 2009.  Hongwei Xi. Examples encoding deduction systems. http:\/\/www.ats-lang.org\/EXAMPLE\/LF\/LF.html 2009."},{"key":"e_1_3_2_1_31_1","unstructured":"Hongwei Xi et al. The ATS language. http:\/\/www.ats-lang.org\/ 2009.  Hongwei Xi et al. The ATS language. http:\/\/www.ats-lang.org\/ 2009."},{"key":"e_1_3_2_1_32_1","first-page":"45","volume-title":"OSDI '06: Proceedings of the 7th symposium on Operating systems design and implementation","author":"Zhou Feng","year":"2006","unstructured":"Feng Zhou , Jeremy Condit , Zachary Anderson , Ilya Bagrak , Rob Ennals , Matthew Harren , George Necula , and Eric Brewer . SafeDrive : safe and recoverable extensions using language-based techniques . In OSDI '06: Proceedings of the 7th symposium on Operating systems design and implementation , pages 45 -- 60 , Berkeley, CA, USA , 2006 . USENIX Association. Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula, and Eric Brewer. SafeDrive: safe and recoverable extensions using language-based techniques. In OSDI '06: Proceedings of the 7th symposium on Operating systems design and implementation, pages 45--60, Berkeley, CA, USA, 2006. USENIX Association."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Madrid Spain","acronym":"POPL '10"},"container-title":["Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1707790.1707793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1707790.1707793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:45:36Z","timestamp":1750250736000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1707790.1707793"}},"subtitle":["work in progress"],"short-title":[],"issued":{"date-parts":[[2010,1,19]]},"references-count":33,"alternative-id":["10.1145\/1707790.1707793","10.1145\/1707790"],"URL":"https:\/\/doi.org\/10.1145\/1707790.1707793","relation":{},"subject":[],"published":{"date-parts":[[2010,1,19]]},"assertion":[{"value":"2010-01-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}