{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:23:30Z","timestamp":1725524610851},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540929949"},{"type":"electronic","value":"9783540929956"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-92995-6_4","type":"book-chapter","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T09:02:58Z","timestamp":1231491778000},"page":"46-60","source":"Crossref","is-referenced-by-count":4,"title":["Toward a Practical Module System for ACL2"],"prefix":"10.1007","author":[{"given":"Carl","family":"Eastlund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Felleisen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","first-page":"146","volume-title":"Automated Reasoning and Its Applications: Essays in Honor of Larry Wos","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Moore, J.S.: Mechanized reasoning about programs and computing machines. In: Veroff, R. (ed.) Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pp. 146\u2013176. MIT Press, Cambridge (1996)"},{"key":"4_CR2","unstructured":"Steele Jr., G.L.: Common Lisp\u2014The Language. Digital Press (1984)"},{"key":"4_CR3","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"4_CR4","first-page":"293","volume-title":"Advanced Topics in Types and Prog. Languages","author":"R. Harper","year":"2004","unstructured":"Harper, R., Pierce, B.C.: Design considerations for ML-style module systems. In: Advanced Topics in Types and Prog. Languages, pp. 293\u2013345. MIT Press, Cambridge (2004)"},{"issue":"6","key":"4_CR5","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1017\/S095679680700634X","volume":"17","author":"R. Page","year":"2007","unstructured":"Page, R.: Engineering software correctness. J. of Func. Prog.\u00a017(6), 675\u2013686 (2007)","journal-title":"J. of Func. Prog."},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1217975.1217999","volume-title":"Proc. 6th Intern. Works. ACL2 Theorem Prover and its Applications","author":"D. Vaillancourt","year":"2006","unstructured":"Vaillancourt, D., Page, R., Felleisen, M.: ACL2 in DrScheme. In: Proc. 6th Intern. Works. ACL2 Theorem Prover and its Applications, pp. 107\u2013116. ACM Press, New York (2006)"},{"key":"4_CR7","first-page":"200","volume-title":"Proc. 7th Intern. ACL2 Workshop","author":"C. Eastlund","year":"2007","unstructured":"Eastlund, C., Vaillancourt, D., Felleisen, M.: ACL2 for freshmen: First experiences. In: Proc. 7th Intern. ACL2 Workshop, pp. 200\u2013211. ACM Press, New York (2007)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Flatt, M., Felleisen, M.: Units: Cool modules for HOT languages. In: ACM SIGPLAN Conference on Prog. Language Design and Implementation, pp. 236\u2013248 (June 1998)","DOI":"10.1145\/277652.277730"},{"key":"4_CR9","first-page":"87","volume-title":"ACM SIGPLAN Intern. Conference on Func. Prog.","author":"S. Owens","year":"2006","unstructured":"Owens, S., Flatt, M.: From structures and functors to modules and units. In: ACM SIGPLAN Intern. Conference on Func. Prog., pp. 87\u201398. ACM Press, New York (2006)"},{"key":"4_CR10","first-page":"282","volume-title":"Proceedings of the International Conference on Computer Languages","author":"G. Bracha","year":"1992","unstructured":"Bracha, G., Lindstrom, G.: Modularity meets inheritance. In: Proceedings of the International Conference on Computer Languages, pp. 282\u2013290. IEEE, Los Alamitos (1992)"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1145\/1411204.1411248","volume-title":"Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming","author":"D. Dreyer","year":"2008","unstructured":"Dreyer, D., Rossberg, A.: Mixin\u2019 up the ML module system. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 307\u2013320. ACM, New York (2008)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrzaszcz","year":"2003","unstructured":"Chrzaszcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S0956796806005867","volume":"17","author":"J. Courant","year":"2006","unstructured":"Courant, J.: $\\mathcal{MC}_2$ : A Module Calculus for Pure Type Systems. J. of Func. Prog.\u00a017, 287\u2013352 (2006)","journal-title":"J. of Func. Prog."},{"issue":"1","key":"4_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/8.1.5","volume":"8","author":"R. Harper","year":"1998","unstructured":"Harper, R., Pfenning, F.: A module system for a programming language based on the LF logical framework. Journal of Logic and Computation\u00a08(1), 5\u201331 (1998)","journal-title":"Journal of Logic and Computation"},{"key":"4_CR15","unstructured":"Sannella, D.: Formal program development in Extended ML for the working programmer. In: Proc. 3rd BCS\/FACS Workshop on Refinement, pp. 99\u2013130 (1991)"},{"key":"4_CR16","volume-title":"The Definition of Standard ML (2e)","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (2e). MIT Press, Cambridge (1990)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"4_CR18","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual (2006), http:\/\/coq.inria.fr\/V8.1pl3\/refman\/index.html"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W.M. Farmer","year":"1993","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: An interactive mathematical proof system. Journal of Automated Reasoning\u00a011, 213\u2013248 (1993)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92995-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:33:27Z","timestamp":1558053207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92995-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540929949","9783540929956"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92995-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}